commit 855ac3eff49e294fd1d2a1c5d039376d706b0f34 Author: Dan Frumin Date: Wed Feb 14 12:55:20 2018 +0100 Initial import from darcs diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..73ac919 --- /dev/null +++ b/.gitignore @@ -0,0 +1,14 @@ +*.vo +*.vio +*.v.d +*.glob +*.cache +*.aux +\#*\# +.\#* +*~ +*.bak +build-dep/ +Makefile.coq +Makefile.coq.conf +*.crashcoqide diff --git a/ArrayMachine.v b/ArrayMachine.v new file mode 100644 index 0000000..b1443ef --- /dev/null +++ b/ArrayMachine.v @@ -0,0 +1,128 @@ +Require Import Rushby. +Require Import list relations collections fin_collections. + +Module ArrayMachine <: Mealy. + +Definition state := nat -> nat. +Inductive command := + | Write : nat -> nat -> command + | Read : nat -> command +. +Definition action := command. +Definition out := nat. + +Definition extendS (s : state) (n : nat) (m : nat) : state := + fun x => if beq_nat x n then m else s x. + +Definition preform (s : state) (a : action) : state * out := + match a with + | Write i j => (extendS s i j, 0) + | Read i => (s, s i) + end. + +Definition step s a := fst (preform s a). +Definition output s a := snd (preform s a). +Definition initial (x : nat) := 0. +End ArrayMachine. + + +Import ArrayMachine. +Module M := Rushby.Rushby ArrayMachine. +Import M. + +Eval compute in (do_actions [Write 1 1] 2). + +Definition domain := action. +Definition nameA := nat. +Definition valA := nat. +Definition observeA (u : domain) : FinSet nameA := + match u with + | Read i => {[ i ]} + | Write _ _ => ∅ + end. +Definition alterA (u : domain) : FinSet valA := + match u with + | Read _ => ∅ + | Write i _ => {[ i ]} + end. + + +Instance domain_dec : forall (u v : domain), Decision (u = v). +Proof. intros. +unfold Decision. +repeat (decide equality). +Defined. + +Instance arraymachine_ss : StructuredState domain := + { name := nameA; value := valA; contents s n := s n + ; observe := observeA; alter := alterA }. + +Definition interference (u v : domain) := + (exists (n : nameA), n ∈ alterA u ∧ n ∈ observeA v). + +Inductive interferenceR : relation domain := + | interference_refl : forall (u : domain), interferenceR u u + | interference_step : forall (u v: domain), interference u v -> interferenceR u v. + +Instance policy_ss : Policy domain := + { policy := interferenceR + ; dom := fun (a : action) => (a : domain) }. +Proof. +intros. unfold Decision. +destruct v as [i j | i]; destruct w as [m n | m]. +- destruct (decide (i = m)). destruct (decide (j = n)); subst; auto. +left. constructor. +right. intro I. inversion I; subst. apply n0. auto. +inversion H. unfold observeA in *. destruct H0 as [HH HHH]. +apply (not_elem_of_empty x); assumption. +right. intro. inversion H; subst. apply n0. auto. +inversion H0. unfold alterA, observeA in *. destruct H1. +apply (not_elem_of_empty x); assumption. +- destruct (decide (i = m)); subst. left. right. unfold interference. + simpl. exists m. split; apply elem_of_singleton; auto. + right. intro. inversion H; subst. inversion H0. simpl in H1. + destruct H1. apply elem_of_singleton in H1; apply elem_of_singleton in H2. subst. apply n;auto. +- right. intro. inversion H;subst. inversion H0; subst. + simpl in H1; inversion H1. apply (not_elem_of_empty x); assumption. +- destruct (decide (i = m)); subst. + left. constructor. + right. intro. inversion H; subst. auto. + inversion H0; subst. simpl in H1; inversion H1. eapply not_elem_of_empty. eassumption. +- intro u. constructor. +Defined. + +Check RefMonAssumptions. + +Instance rma_yay : RefMonAssumptions. +Proof. split; simpl; unfold RMA_partition; intros; + unfold contents in *; simpl in H8. +unfold output. + unfold preform. destruct a as [i j | i]; simpl in *. reflexivity. + apply H8. apply elem_of_singleton. reflexivity. + +unfold step, preform. destruct a as [i j | i]. simpl in *. +destruct (decide (i = n)); subst; unfold extendS; simpl. +replace (beq_nat n n) with true; auto. apply beq_nat_refl. +destruct H9. +unfold step in H9; simpl in H9. unfold extendS in H9; simpl in H9. +replace (beq_nat n i) with false in *; auto. +congruence. SearchAbout beq_nat false. symmetry. apply beq_nat_false_iff. omega. +unfold step in H9; simpl in H9. unfold extendS in H9; simpl in H9. +replace (beq_nat n i) with false in *; auto. +congruence. symmetry. apply beq_nat_false_iff. omega. + +simpl. destruct H9; unfold step, preform in H9; simpl in H9; + congruence. + +unfold step, preform in H8; simpl in H8. destruct a; simpl in *. +unfold extendS in H8. destruct (decide (n = n0)); subst. +apply elem_of_singleton; auto. replace (beq_nat n n0) with false in *; try (congruence). symmetry. apply beq_nat_false_iff. assumption. +congruence. +Defined. + +Theorem yay : isecurity. +Proof. + apply rma_secure_intransitive. + intros u v n A1 A2. simpl. right. firstorder. +Qed. + diff --git a/LibTactics.v b/LibTactics.v new file mode 100755 index 0000000..1e3ddbd --- /dev/null +++ b/LibTactics.v @@ -0,0 +1,5004 @@ +(** * LibTactics: A Collection of Handy General-Purpose Tactics *) + +(* Chapter maintained by Arthur Chargueraud *) + +(** This file contains a set of tactics that extends the set of builtin + tactics provided with the standard distribution of Coq. It intends + to overcome a number of limitations of the standard set of tactics, + and thereby to help user to write shorter and more robust scripts. + + Hopefully, Coq tactics will be improved as time goes by, and this + file should ultimately be useless. In the meanwhile, serious Coq + users will probably find it very useful. + + The present file contains the implementation and the detailed + documentation of those tactics. The SF reader need not read this + file; instead, he/she is encouraged to read the chapter named + UseTactics.v, which is gentle introduction to the most useful + tactics from the LibTactic library. *) + +(** The main features offered are: + - More convenient syntax for naming hypotheses, with tactics for + introduction and inversion that take as input only the name of + hypotheses of type [Prop], rather than the name of all variables. + - Tactics providing true support for manipulating N-ary conjunctions, + disjunctions and existentials, hidding the fact that the underlying + implementation is based on binary propositions. + - Convenient support for automation: tactic followed with the symbol + "~" or "*" will call automation on the generated subgoals. + Symbol "~" stands for [auto] and "*" for [intuition eauto]. + These bindings can be customized. + - Forward-chaining tactics are provided to instantiate lemmas + either with variable or hypotheses or a mix of both. + - A more powerful implementation of [apply] is provided (it is based + on [refine] and thus behaves better with respect to conversion). + - An improved inversion tactic which substitutes equalities on variables + generated by the standard inversion mecanism. Moreover, it supports + the elimination of dependently-typed equalities (requires axiom [K], + which is a weak form of Proof Irrelevance). + - Tactics for saving time when writing proofs, with tactics to + asserts hypotheses or sub-goals, and improved tactics for + clearing, renaming, and sorting hypotheses. +*) + +(** External credits: + - thanks to Xavier Leroy for providing the idea of tactic [forward], + - thanks to Georges Gonthier for the implementation trick in [rapply], +*) + +Set Implicit Arguments. + +Require Import List. + +(* Very important to remove hint trans_eq_bool from LibBool, + otherwise eauto slows down dramatically: + Lemma test : forall b, b = false. + time eauto 7. (* takes over 4 seconds to fail! *) *) + +Remove Hints Bool.trans_eq_bool. + + +(* ********************************************************************** *) +(** * Tools for programming with Ltac *) + +(* ---------------------------------------------------------------------- *) +(** ** Identity continuation *) + +Ltac idcont tt := + idtac. + +(* ---------------------------------------------------------------------- *) +(** ** Untyped arguments for tactics *) + +(** Any Coq value can be boxed into the type [Boxer]. This is + useful to use Coq computations for implementing tactics. *) + +Inductive Boxer : Type := + | boxer : forall (A:Type), A -> Boxer. + + +(* ---------------------------------------------------------------------- *) +(** ** Optional arguments for tactics *) + +(** [ltac_no_arg] is a constant that can be used to simulate + optional arguments in tactic definitions. + Use [mytactic ltac_no_arg] on the tactic invokation, + and use [match arg with ltac_no_arg => ..] or + [match type of arg with ltac_No_arg => ..] to + test whether an argument was provided. *) + +Inductive ltac_No_arg : Set := + | ltac_no_arg : ltac_No_arg. + + +(* ---------------------------------------------------------------------- *) +(** ** Wildcard arguments for tactics *) + +(** [ltac_wild] is a constant that can be used to simulate + wildcard arguments in tactic definitions. Notation is [__]. *) + +Inductive ltac_Wild : Set := + | ltac_wild : ltac_Wild. + +Notation "'__'" := ltac_wild : ltac_scope. + +(** [ltac_wilds] is another constant that is typically used to + simulate a sequence of [N] wildcards, with [N] chosen + appropriately depending on the context. Notation is [___]. *) + +Inductive ltac_Wilds : Set := + | ltac_wilds : ltac_Wilds. + +Notation "'___'" := ltac_wilds : ltac_scope. + +Open Scope ltac_scope. + + +(* ---------------------------------------------------------------------- *) +(** ** Position markers *) + +(** [ltac_Mark] and [ltac_mark] are dummy definitions used as sentinel + by tactics, to mark a certain position in the context or in the goal. *) + +Inductive ltac_Mark : Type := + | ltac_mark : ltac_Mark. + +(** [gen_until_mark] repeats [generalize] on hypotheses from the + context, starting from the bottom and stopping as soon as reaching + an hypothesis of type [Mark]. If fails if [Mark] does not + appear in the context. *) + +Ltac gen_until_mark := + match goal with H: ?T |- _ => + match T with + | ltac_Mark => clear H + | _ => generalize H; clear H; gen_until_mark + end end. + +(** [intro_until_mark] repeats [intro] until reaching an hypothesis of + type [Mark]. It throws away the hypothesis [Mark]. + It fails if [Mark] does not appear as an hypothesis in the + goal. *) + +Ltac intro_until_mark := + match goal with + | |- (ltac_Mark -> _) => intros _ + | _ => intro; intro_until_mark + end. + + +(* ---------------------------------------------------------------------- *) +(** ** List of arguments for tactics *) + +(** A datatype of type [list Boxer] is used to manipulate list of + Coq values in ltac. Notation is [>> v1 v2 ... vN] for building + a list containing the values [v1] through [vN]. *) + +Notation "'>>'" := + (@nil Boxer) + (at level 0) + : ltac_scope. +Notation "'>>' v1" := + ((boxer v1)::nil) + (at level 0, v1 at level 0) + : ltac_scope. +Notation "'>>' v1 v2" := + ((boxer v1)::(boxer v2)::nil) + (at level 0, v1 at level 0, v2 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3" := + ((boxer v1)::(boxer v2)::(boxer v3)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4 v5" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::(boxer v5)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0, v5 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4 v5 v6" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::(boxer v5) + ::(boxer v6)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0, v5 at level 0, v6 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4 v5 v6 v7" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::(boxer v5) + ::(boxer v6)::(boxer v7)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0, v5 at level 0, v6 at level 0, v7 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4 v5 v6 v7 v8" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::(boxer v5) + ::(boxer v6)::(boxer v7)::(boxer v8)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0, v5 at level 0, v6 at level 0, v7 at level 0, + v8 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4 v5 v6 v7 v8 v9" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::(boxer v5) + ::(boxer v6)::(boxer v7)::(boxer v8)::(boxer v9)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0, v5 at level 0, v6 at level 0, v7 at level 0, + v8 at level 0, v9 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4 v5 v6 v7 v8 v9 v10" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::(boxer v5) + ::(boxer v6)::(boxer v7)::(boxer v8)::(boxer v9)::(boxer v10)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0, v5 at level 0, v6 at level 0, v7 at level 0, + v8 at level 0, v9 at level 0, v10 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::(boxer v5) + ::(boxer v6)::(boxer v7)::(boxer v8)::(boxer v9)::(boxer v10) + ::(boxer v11)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0, v5 at level 0, v6 at level 0, v7 at level 0, + v8 at level 0, v9 at level 0, v10 at level 0, v11 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::(boxer v5) + ::(boxer v6)::(boxer v7)::(boxer v8)::(boxer v9)::(boxer v10) + ::(boxer v11)::(boxer v12)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0, v5 at level 0, v6 at level 0, v7 at level 0, + v8 at level 0, v9 at level 0, v10 at level 0, v11 at level 0, + v12 at level 0) + : ltac_scope. +Notation "'>>' v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13" := + ((boxer v1)::(boxer v2)::(boxer v3)::(boxer v4)::(boxer v5) + ::(boxer v6)::(boxer v7)::(boxer v8)::(boxer v9)::(boxer v10) + ::(boxer v11)::(boxer v12)::(boxer v13)::nil) + (at level 0, v1 at level 0, v2 at level 0, v3 at level 0, + v4 at level 0, v5 at level 0, v6 at level 0, v7 at level 0, + v8 at level 0, v9 at level 0, v10 at level 0, v11 at level 0, + v12 at level 0, v13 at level 0) + : ltac_scope. + + +(** The tactic [list_boxer_of] inputs a term [E] and returns a term + of type "list boxer", according to the following rules: + - if [E] is already of type "list Boxer", then it returns [E]; + - otherwise, it returns the list [(boxer E)::nil]. *) + +Ltac list_boxer_of E := + match type of E with + | List.list Boxer => constr:(E) + | _ => constr:((boxer E)::nil) + end. + + +(* ---------------------------------------------------------------------- *) +(** ** Databases of lemmas *) + +(** Use the hint facility to implement a database mapping + terms to terms. To declare a new database, use a definition: + [Definition mydatabase := True.] + + Then, to map [mykey] to [myvalue], write the hint: + [Hint Extern 1 (Register mydatabase mykey) => Provide myvalue.] + + Finally, to query the value associated with a key, run the + tactic [ltac_database_get mydatabase mykey]. This will leave + at the head of the goal the term [myvalue]. It can then be + named and exploited using [intro]. *) + +Inductive Ltac_database_token : Prop := ltac_database_token. + +Definition ltac_database (D:Boxer) (T:Boxer) (A:Boxer) := Ltac_database_token. + +Notation "'Register' D T" := (ltac_database (boxer D) (boxer T) _) + (at level 69, D at level 0, T at level 0). + +Lemma ltac_database_provide : forall (A:Boxer) (D:Boxer) (T:Boxer), + ltac_database D T A. +Proof using. split. Qed. + +Ltac Provide T := apply (@ltac_database_provide (boxer T)). + +Ltac ltac_database_get D T := + let A := fresh "TEMP" in evar (A:Boxer); + let H := fresh "TEMP" in + assert (H : ltac_database (boxer D) (boxer T) A); + [ subst A; auto + | subst A; match type of H with ltac_database _ _ (boxer ?L) => + generalize L end; clear H ]. + +(* Note for a possible alternative implementation of the ltac_database_token: + Inductive Ltac_database : Type := + | ltac_database : forall A, A -> Ltac_database. + Implicit Arguments ltac_database [A]. +*) + +(* ---------------------------------------------------------------------- *) +(** ** On-the-fly removal of hypotheses *) + +(** In a list of arguments [>> H1 H2 .. HN] passed to a tactic + such as [lets] or [applys] or [forwards] or [specializes], + the term [rm], an identity function, can be placed in front + of the name of an hypothesis to be deleted. *) + +Definition rm (A:Type) (X:A) := X. + +(** [rm_term E] removes one hypothesis that admits the same + type as [E]. *) + +Ltac rm_term E := + let T := type of E in + match goal with H: T |- _ => try clear H end. + +(** [rm_inside E] calls [rm_term Ei] for any subterm + of the form [rm Ei] found in E *) + +Ltac rm_inside E := + let go E := rm_inside E in + match E with + | rm ?X => rm_term X + | ?X1 ?X2 => + go X1; go X2 + | ?X1 ?X2 ?X3 => + go X1; go X2; go X3 + | ?X1 ?X2 ?X3 ?X4 => + go X1; go X2; go X3; go X4 + | ?X1 ?X2 ?X3 ?X4 ?X5 => + go X1; go X2; go X3; go X4; go X5 + | ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 => + go X1; go X2; go X3; go X4; go X5; go X6 + | ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X7 => + go X1; go X2; go X3; go X4; go X5; go X6; go X7 + | ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X7 ?X8 => + go X1; go X2; go X3; go X4; go X5; go X6; go X7; go X8 + | ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X7 ?X8 ?X9 => + go X1; go X2; go X3; go X4; go X5; go X6; go X7; go X8; go X9 + | ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X7 ?X8 ?X9 ?X10 => + go X1; go X2; go X3; go X4; go X5; go X6; go X7; go X8; go X9; go X10 + | _ => idtac + end. + +(** For faster performance, one may deactivate [rm_inside] by + replacing the body of this definition with [idtac]. *) + +Ltac fast_rm_inside E := + rm_inside E. + + +(* ---------------------------------------------------------------------- *) +(** ** Numbers as arguments *) + +(** When tactic takes a natural number as argument, it may be + parsed either as a natural number or as a relative number. + In order for tactics to convert their arguments into natural numbers, + we provide a conversion tactic. *) + +(* COQ-8.4: + Require Coq.Numbers.BinNums Coq.ZArith.BinInt. *) +Require BinPos Coq.ZArith.BinInt. + +Definition ltac_nat_from_int (x:BinInt.Z) : nat := + match x with + | BinInt.Z0 => 0%nat + | BinInt.Zpos p => BinPos.nat_of_P p + | BinInt.Zneg p => 0%nat + end. + +Ltac nat_from_number N := + match type of N with + | nat => constr:(N) + | BinInt.Z => let N' := constr:(ltac_nat_from_int N) in eval compute in N' + end. + +(** [ltac_pattern E at K] is the same as [pattern E at K] except that + [K] is a Coq natural rather than a Ltac integer. Syntax + [ltac_pattern E as K in H] is also available. *) + +Tactic Notation "ltac_pattern" constr(E) "at" constr(K) := + match nat_from_number K with + | 1 => pattern E at 1 + | 2 => pattern E at 2 + | 3 => pattern E at 3 + | 4 => pattern E at 4 + | 5 => pattern E at 5 + | 6 => pattern E at 6 + | 7 => pattern E at 7 + | 8 => pattern E at 8 + end. + +Tactic Notation "ltac_pattern" constr(E) "at" constr(K) "in" hyp(H) := + match nat_from_number K with + | 1 => pattern E at 1 in H + | 2 => pattern E at 2 in H + | 3 => pattern E at 3 in H + | 4 => pattern E at 4 in H + | 5 => pattern E at 5 in H + | 6 => pattern E at 6 in H + | 7 => pattern E at 7 in H + | 8 => pattern E at 8 in H + end. + + +(* ---------------------------------------------------------------------- *) +(** ** Testing tactics *) + +(** [show tac] executes a tactic [tac] that produces a result, + and then display its result. *) + +Tactic Notation "show" tactic(tac) := + let R := tac in pose R. + +(** [dup N] produces [N] copies of the current goal. It is useful + for building examples on which to illustrate behaviour of tactics. + [dup] is short for [dup 2]. *) + +Lemma dup_lemma : forall P, P -> P -> P. +Proof using. auto. Qed. + +Ltac dup_tactic N := + match nat_from_number N with + | 0 => idtac + | S 0 => idtac + | S ?N' => apply dup_lemma; [ | dup_tactic N' ] + end. + +Tactic Notation "dup" constr(N) := + dup_tactic N. +Tactic Notation "dup" := + dup 2. + + +(* ---------------------------------------------------------------------- *) +(** ** Check no evar in goal *) + +(* COQ8.4: +Ltac check_noevar M := + match M with M => idtac end. + +Ltac check_noevar_hyp H := (* todo: imlement using check_noevar *) + let T := type of H in + match type of H with T => idtac end. + +Ltac check_noevar_goal := (* todo: imlement using check_noevar *) + match goal with |- ?G => match G with G => idtac end end. +*) +Ltac check_noevar M := + first [ has_evar M; fail 2 | idtac ]. + +Ltac check_noevar_hyp H := (* todo: imlement using check_noevar *) + let T := type of H in check_noevar T. +Ltac check_noevar_goal := (* todo: imlement using check_noevar *) + match goal with |- ?G => check_noevar G end. + +(* ---------------------------------------------------------------------- *) +(** ** Helper function for introducing evars *) + +(** [with_evar T (fun M => tac)] creates a new evar that can + be used in the tactic [tac] under the name [M]. *) + +Ltac with_evar_base T cont := + let x := fresh in evar (x:T); cont x; subst x. + +Tactic Notation "with_evar" constr(T) tactic(cont) := + with_evar_base T cont. + + +(* ---------------------------------------------------------------------- *) +(** ** Tagging of hypotheses *) + +(** [get_last_hyp tt] is a function that returns the last hypothesis + at the bottom of the context. It is useful to obtain the default + name associated with the hypothesis, e.g. + [intro; let H := get_last_hyp tt in let H' := fresh "P" H in ...] *) + +Ltac get_last_hyp tt := + match goal with H: _ |- _ => constr:(H) end. + + +(* ---------------------------------------------------------------------- *) +(** ** Tagging of hypotheses *) + +(** [ltac_tag_subst] is a specific marker for hypotheses + which is used to tag hypotheses that are equalities to + be substituted. *) + +Definition ltac_tag_subst (A:Type) (x:A) := x. + +(** [ltac_to_generalize] is a specific marker for hypotheses + to be generalized. *) + +Definition ltac_to_generalize (A:Type) (x:A) := x. + +Ltac gen_to_generalize := + repeat match goal with + H: ltac_to_generalize _ |- _ => generalize H; clear H end. + +Ltac mark_to_generalize H := + let T := type of H in + change T with (ltac_to_generalize T) in H. + + +(* ---------------------------------------------------------------------- *) +(** ** Deconstructing terms *) + +(** [get_head E] is a tactic that returns the head constant of the + term [E], ie, when applied to a term of the form [P x1 ... xN] + it returns [P]. If [E] is not an application, it returns [E]. + Warning: the tactic seems to loop in some cases when the goal is + a product and one uses the result of this function. *) + +Ltac get_head E := + match E with + | ?P _ _ _ _ _ _ _ _ _ _ _ _ => constr:(P) + | ?P _ _ _ _ _ _ _ _ _ _ _ => constr:(P) + | ?P _ _ _ _ _ _ _ _ _ _ => constr:(P) + | ?P _ _ _ _ _ _ _ _ _ => constr:(P) + | ?P _ _ _ _ _ _ _ _ => constr:(P) + | ?P _ _ _ _ _ _ _ => constr:(P) + | ?P _ _ _ _ _ _ => constr:(P) + | ?P _ _ _ _ _ => constr:(P) + | ?P _ _ _ _ => constr:(P) + | ?P _ _ _ => constr:(P) + | ?P _ _ => constr:(P) + | ?P _ => constr:(P) + | ?P => constr:(P) + end. + +(** [get_fun_arg E] is a tactic that decomposes an application + term [E], ie, when applied to a term of the form [X1 ... XN] + it returns a pair made of [X1 .. X(N-1)] and [XN]. *) + +Ltac get_fun_arg E := + match E with + | ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X7 ?X => constr:((X1 X2 X3 X4 X5 X6,X)) + | ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X => constr:((X1 X2 X3 X4 X5,X)) + | ?X1 ?X2 ?X3 ?X4 ?X5 ?X => constr:((X1 X2 X3 X4,X)) + | ?X1 ?X2 ?X3 ?X4 ?X => constr:((X1 X2 X3,X)) + | ?X1 ?X2 ?X3 ?X => constr:((X1 X2,X)) + | ?X1 ?X2 ?X => constr:((X1,X)) + | ?X1 ?X => constr:((X1,X)) + end. + + +(* ---------------------------------------------------------------------- *) +(** ** Action at occurence and action not at occurence *) + +(** [ltac_action_at K of E do Tac] isolates the [K]-th occurence of [E] in the + goal, setting it in the form [P E] for some named pattern [P], + then calls tactic [Tac], and finally unfolds [P]. Syntax + [ltac_action_at K of E in H do Tac] is also available. *) + +Tactic Notation "ltac_action_at" constr(K) "of" constr(E) "do" tactic(Tac) := + let p := fresh in ltac_pattern E at K; + match goal with |- ?P _ => set (p:=P) end; + Tac; unfold p; clear p. + +Tactic Notation "ltac_action_at" constr(K) "of" constr(E) "in" hyp(H) "do" tactic(Tac) := + let p := fresh in ltac_pattern E at K in H; + match type of H with ?P _ => set (p:=P) in H end; + Tac; unfold p in H; clear p. + +(** [protects E do Tac] temporarily assigns a name to the expression [E] + so that the execution of tactic [Tac] will not modify [E]. This is + useful for instance to restrict the action of [simpl]. *) + +Tactic Notation "protects" constr(E) "do" tactic(Tac) := + (* let x := fresh "TEMP" in sets_eq x: E; T; subst x. *) + let x := fresh "TEMP" in let H := fresh "TEMP" in + set (X := E) in *; assert (H : X = E) by reflexivity; + clearbody X; Tac; subst x. + +Tactic Notation "protects" constr(E) "do" tactic(Tac) "/" := + protects E do Tac. + +(* ---------------------------------------------------------------------- *) +(** ** An alias for [eq] *) + +(** [eq'] is an alias for [eq] to be used for equalities in + inductive definitions, so that they don't get mixed with + equalities generated by [inversion]. *) + +Definition eq' := @eq. + +Hint Unfold eq'. + +Notation "x '='' y" := (@eq' _ x y) + (at level 70, y at next level). + + +(* ********************************************************************** *) +(** * Common tactics for simplifying goals like [intuition] *) + +Ltac jauto_set_hyps := + repeat match goal with H: ?T |- _ => + match T with + | _ /\ _ => destruct H + | exists a, _ => destruct H + | _ => generalize H; clear H + end + end. + +Ltac jauto_set_goal := + repeat match goal with + | |- exists a, _ => esplit + | |- _ /\ _ => split + end. + +Ltac jauto_set := + intros; jauto_set_hyps; + intros; jauto_set_goal; + unfold not in *. + + + +(* ********************************************************************** *) +(** * Backward and forward chaining *) + +(* ---------------------------------------------------------------------- *) +(** ** Application *) + +Ltac old_refine f := + refine f. (* ; shelve_unifiable. *) + +(** [rapply] is a tactic similar to [eapply] except that it is + based on the [refine] tactics, and thus is strictly more + powerful (at least in theory :). In short, it is able to perform + on-the-fly conversions when required for arguments to match, + and it is able to instantiate existentials when required. *) + +Tactic Notation "rapply" constr(t) := + first (* todo: les @ sont inutiles *) + [ eexact (@t) + | refine (@t) + | refine (@t _) + | refine (@t _ _) + | refine (@t _ _ _) + | refine (@t _ _ _ _) + | refine (@t _ _ _ _ _) + | refine (@t _ _ _ _ _ _) + | refine (@t _ _ _ _ _ _ _) + | refine (@t _ _ _ _ _ _ _ _) + | refine (@t _ _ _ _ _ _ _ _ _) + | refine (@t _ _ _ _ _ _ _ _ _ _) + | refine (@t _ _ _ _ _ _ _ _ _ _ _) + | refine (@t _ _ _ _ _ _ _ _ _ _ _ _) + | refine (@t _ _ _ _ _ _ _ _ _ _ _ _ _) + | refine (@t _ _ _ _ _ _ _ _ _ _ _ _ _ _) + | refine (@t _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) + ]. + +(** The tactics [applys_N T], where [N] is a natural number, + provides a more efficient way of using [applys T]. It avoids + trying out all possible arities, by specifying explicitely + the arity of function [T]. *) + +Tactic Notation "rapply_0" constr(t) := + refine (@t). +Tactic Notation "rapply_1" constr(t) := + refine (@t _). +Tactic Notation "rapply_2" constr(t) := + refine (@t _ _). +Tactic Notation "rapply_3" constr(t) := + refine (@t _ _ _). +Tactic Notation "rapply_4" constr(t) := + refine (@t _ _ _ _). +Tactic Notation "rapply_5" constr(t) := + refine (@t _ _ _ _ _). +Tactic Notation "rapply_6" constr(t) := + refine (@t _ _ _ _ _ _). +Tactic Notation "rapply_7" constr(t) := + refine (@t _ _ _ _ _ _ _). +Tactic Notation "rapply_8" constr(t) := + refine (@t _ _ _ _ _ _ _ _). +Tactic Notation "rapply_9" constr(t) := + refine (@t _ _ _ _ _ _ _ _ _). +Tactic Notation "rapply_10" constr(t) := + refine (@t _ _ _ _ _ _ _ _ _ _). + +(** [lets_base H E] adds an hypothesis [H : T] to the context, where [T] is + the type of term [E]. If [H] is an introduction pattern, it will + destruct [H] according to the pattern. *) + +Ltac lets_base I E := generalize E; intros I. + +(** [applys_to H E] transform the type of hypothesis [H] by + replacing it by the result of the application of the term + [E] to [H]. Intuitively, it is equivalent to [lets H: (E H)]. *) + +Tactic Notation "applys_to" hyp(H) constr(E) := + let H' := fresh in rename H into H'; + (first [ lets_base H (E H') + | lets_base H (E _ H') + | lets_base H (E _ _ H') + | lets_base H (E _ _ _ H') + | lets_base H (E _ _ _ _ H') + | lets_base H (E _ _ _ _ _ H') + | lets_base H (E _ _ _ _ _ _ H') + | lets_base H (E _ _ _ _ _ _ _ H') + | lets_base H (E _ _ _ _ _ _ _ _ H') + | lets_base H (E _ _ _ _ _ _ _ _ _ H') ] + ); clear H'. + +(** [applys_to H1,...,HN E] applys [E] to several hypotheses *) + +Tactic Notation "applys_to" hyp(H1) "," hyp(H2) constr(E) := + applys_to H1 E; applys_to H2 E. +Tactic Notation "applys_to" hyp(H1) "," hyp(H2) "," hyp(H3) constr(E) := + applys_to H1 E; applys_to H2 E; applys_to H3 E. +Tactic Notation "applys_to" hyp(H1) "," hyp(H2) "," hyp(H3) "," hyp(H4) constr(E) := + applys_to H1 E; applys_to H2 E; applys_to H3 E; applys_to H4 E. + +(** [constructors] calls [constructor] or [econstructor]. *) + +Tactic Notation "constructors" := + first [ constructor | econstructor ]; unfold eq'. + +(* ---------------------------------------------------------------------- *) +(** ** Assertions *) + +(** [asserts H: T] is another syntax for [assert (H : T)], which + also works with introduction patterns. For instance, one can write: + [asserts \[x P\] (exists n, n = 3)], or + [asserts \[H|H\] (n = 0 \/ n = 1). *) + +Tactic Notation "asserts" simple_intropattern(I) ":" constr(T) := + let H := fresh in assert (H : T); + [ | generalize H; clear H; intros I ]. + +(** [asserts H1 .. HN: T] is a shorthand for + [asserts \[H1 \[H2 \[.. HN\]\]\]\]: T]. *) + +Tactic Notation "asserts" simple_intropattern(I1) + simple_intropattern(I2) ":" constr(T) := + asserts [I1 I2]: T. +Tactic Notation "asserts" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) ":" constr(T) := + asserts [I1 [I2 I3]]: T. +Tactic Notation "asserts" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) + simple_intropattern(I4) ":" constr(T) := + asserts [I1 [I2 [I3 I4]]]: T. +Tactic Notation "asserts" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) + simple_intropattern(I4) simple_intropattern(I5) ":" constr(T) := + asserts [I1 [I2 [I3 [I4 I5]]]]: T. +Tactic Notation "asserts" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) + simple_intropattern(I4) simple_intropattern(I5) + simple_intropattern(I6) ":" constr(T) := + asserts [I1 [I2 [I3 [I4 [I5 I6]]]]]: T. + +(** [asserts: T] is [asserts H: T] with [H] being chosen automatically. *) + +Tactic Notation "asserts" ":" constr(T) := + let H := fresh in asserts H : T. + +(** [cuts H: T] is the same as [asserts H: T] except that the two subgoals + generated are swapped: the subgoal [T] comes second. Note that contrary + to [cut], it introduces the hypothesis. *) + +Tactic Notation "cuts" simple_intropattern(I) ":" constr(T) := + cut (T); [ intros I | idtac ]. + +(** [cuts: T] is [cuts H: T] with [H] being chosen automatically. *) + +Tactic Notation "cuts" ":" constr(T) := + let H := fresh in cuts H: T. + +(** [cuts H1 .. HN: T] is a shorthand for + [cuts \[H1 \[H2 \[.. HN\]\]\]\]: T]. *) + +Tactic Notation "cuts" simple_intropattern(I1) + simple_intropattern(I2) ":" constr(T) := + cuts [I1 I2]: T. +Tactic Notation "cuts" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) ":" constr(T) := + cuts [I1 [I2 I3]]: T. +Tactic Notation "cuts" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) + simple_intropattern(I4) ":" constr(T) := + cuts [I1 [I2 [I3 I4]]]: T. +Tactic Notation "cuts" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) + simple_intropattern(I4) simple_intropattern(I5) ":" constr(T) := + cuts [I1 [I2 [I3 [I4 I5]]]]: T. +Tactic Notation "cuts" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) + simple_intropattern(I4) simple_intropattern(I5) + simple_intropattern(I6) ":" constr(T) := + cuts [I1 [I2 [I3 [I4 [I5 I6]]]]]: T. + + +(* ---------------------------------------------------------------------- *) +(** ** Instantiation and forward-chaining *) + +(** The instantiation tactics are used to instantiate a lemma [E] + (whose type is a product) on some arguments. The type of [E] is + made of implications and universal quantifications, e.g. + [forall x, P x -> forall y z, Q x y z -> R z]. + + The first possibility is to provide arguments in order: first [x], + then a proof of [P x], then [y] etc... In this mode, called "Args", + all the arguments are to be provided. If a wildcard is provided + (written [__]), then an existential variable will be introduced in + place of the argument. + + It is very convenient to give some arguments the lemma should be + instantiated on, and let the tactic find out automatically where + underscores should be insterted. Underscore arguments [__] are + interpret as follows: an underscore means that we want to skip the + argument that has the same type as the next real argument provided + (real means not an underscore). If there is no real argument after + underscore, then the underscore is used for the first possible argument. + + The general syntax is [tactic (>> E1 .. EN)] where [tactic] is + the name of the tactic (possibly with some arguments) and [Ei] + are the arguments. Moreover, some tactics accept the syntax + [tactic E1 .. EN] as short for [tactic (>> E1 .. EN)] for + values of [N] up to 5. + + Finally, if the argument [EN] given is a triple-underscore [___], + then it is equivalent to providing a list of wildcards, with + the appropriate number of wildcards. This means that all + the remaining arguments of the lemma will be instantiated. + Definitions in the conclusion are not unfolded in this case. *) + +(* Underlying implementation *) + +Ltac app_assert t P cont := + let H := fresh "TEMP" in + assert (H : P); [ | cont(t H); clear H ]. + +Ltac app_evar t A cont := + let x := fresh "TEMP" in + evar (x:A); + let t' := constr:(t x) in + let t'' := (eval unfold x in t') in + subst x; cont t''. + +Ltac app_arg t P v cont := + let H := fresh "TEMP" in + assert (H : P); [ apply v | cont(t H); try clear H ]. + +Ltac build_app_alls t final := + let rec go t := + match type of t with + | ?P -> ?Q => app_assert t P go + | forall _:?A, _ => app_evar t A go + | _ => final t + end in + go t. + +Ltac boxerlist_next_type vs := + match vs with + | nil => constr:(ltac_wild) + | (boxer ltac_wild)::?vs' => boxerlist_next_type vs' + | (boxer ltac_wilds)::_ => constr:(ltac_wild) + | (@boxer ?T _)::_ => constr:(T) + end. + +(* Note: refuse to instantiate a dependent hypothesis with a proposition; + refuse to instantiate an argument of type Type with one that + does not have the type Type. +*) + +Ltac build_app_hnts t vs final := + let rec go t vs := + match vs with + | nil => first [ final t | fail 1 ] + | (boxer ltac_wilds)::_ => first [ build_app_alls t final | fail 1 ] + | (boxer ?v)::?vs' => + let cont t' := go t' vs in + let cont' t' := go t' vs' in + let T := type of t in + let T := eval hnf in T in + match v with + | ltac_wild => + first [ let U := boxerlist_next_type vs' in + match U with + | ltac_wild => + match T with + | ?P -> ?Q => first [ app_assert t P cont' | fail 3 ] + | forall _:?A, _ => first [ app_evar t A cont' | fail 3 ] + end + | _ => + match T with (* should test T for unifiability *) + | U -> ?Q => first [ app_assert t U cont' | fail 3 ] + | forall _:U, _ => first [ app_evar t U cont' | fail 3 ] + | ?P -> ?Q => first [ app_assert t P cont | fail 3 ] + | forall _:?A, _ => first [ app_evar t A cont | fail 3 ] + end + end + | fail 2 ] + | _ => + match T with + | ?P -> ?Q => first [ app_arg t P v cont' + | app_assert t P cont + | fail 3 ] + | forall _:Type, _ => + match type of v with + | Type => first [ cont' (t v) + | app_evar t Type cont + | fail 3 ] + | _ => first [ app_evar t Type cont + | fail 3 ] + end + | forall _:?A, _ => + let V := type of v in + match type of V with + | Prop => first [ app_evar t A cont + | fail 3 ] + | _ => first [ cont' (t v) + | app_evar t A cont + | fail 3 ] + end + end + end + end in + go t vs. + + +(** newer version : support for typeclasses *) + +Ltac app_typeclass t cont := + let t' := constr:(t _) in + cont t'. + +Ltac build_app_alls t final ::= + let rec go t := + match type of t with + | ?P -> ?Q => app_assert t P go + | forall _:?A, _ => + first [ app_evar t A go + | app_typeclass t go + | fail 3 ] + | _ => final t + end in + go t. + +Ltac build_app_hnts t vs final ::= + let rec go t vs := + match vs with + | nil => first [ final t | fail 1 ] + | (boxer ltac_wilds)::_ => first [ build_app_alls t final | fail 1 ] + | (boxer ?v)::?vs' => + let cont t' := go t' vs in + let cont' t' := go t' vs' in + let T := type of t in + let T := eval hnf in T in + match v with + | ltac_wild => + first [ let U := boxerlist_next_type vs' in + match U with + | ltac_wild => + match T with + | ?P -> ?Q => first [ app_assert t P cont' | fail 3 ] + | forall _:?A, _ => first [ app_typeclass t cont' + | app_evar t A cont' + | fail 3 ] + end + | _ => + match T with (* should test T for unifiability *) + | U -> ?Q => first [ app_assert t U cont' | fail 3 ] + | forall _:U, _ => first + [ app_typeclass t cont' + | app_evar t U cont' + | fail 3 ] + | ?P -> ?Q => first [ app_assert t P cont | fail 3 ] + | forall _:?A, _ => first + [ app_typeclass t cont + | app_evar t A cont + | fail 3 ] + end + end + | fail 2 ] + | _ => + match T with + | ?P -> ?Q => first [ app_arg t P v cont' + | app_assert t P cont + | fail 3 ] + | forall _:Type, _ => + match type of v with + | Type => first [ cont' (t v) + | app_evar t Type cont + | fail 3 ] + | _ => first [ app_evar t Type cont + | fail 3 ] + end + | forall _:?A, _ => + let V := type of v in + match type of V with + | Prop => first [ app_typeclass t cont + | app_evar t A cont + | fail 3 ] + | _ => first [ cont' (t v) + | app_typeclass t cont + | app_evar t A cont + | fail 3 ] + end + end + end + end in + go t vs. + (* todo: use local function for first [...] *) + + +(*--old version +Ltac build_app_hnts t vs final := + let rec go t vs := + match vs with + | nil => first [ final t | fail 1 ] + | (boxer ltac_wilds)::_ => first [ build_app_alls t final | fail 1 ] + | (boxer ?v)::?vs' => + let cont t' := go t' vs in + let cont' t' := go t' vs' in + let T := type of t in + let T := eval hnf in T in + match v with + | ltac_wild => + first [ let U := boxerlist_next_type vs' in + match U with + | ltac_wild => + match T with + | ?P -> ?Q => first [ app_assert t P cont' | fail 3 ] + | forall _:?A, _ => first [ app_evar t A cont' | fail 3 ] + end + | _ => + match T with (* should test T for unifiability *) + | U -> ?Q => first [ app_assert t U cont' | fail 3 ] + | forall _:U, _ => first [ app_evar t U cont' | fail 3 ] + | ?P -> ?Q => first [ app_assert t P cont | fail 3 ] + | forall _:?A, _ => first [ app_evar t A cont | fail 3 ] + end + end + | fail 2 ] + | _ => + match T with + | ?P -> ?Q => first [ app_arg t P v cont' + | app_assert t P cont + | fail 3 ] + | forall _:?A, _ => first [ cont' (t v) + | app_evar t A cont + | fail 3 ] + end + end + end in + go t vs. +*) + + +Ltac build_app args final := + first [ + match args with (@boxer ?T ?t)::?vs => + let t := constr:(t:T) in + build_app_hnts t vs final; + fast_rm_inside args + end + | fail 1 "Instantiation fails for:" args]. + +Ltac unfold_head_until_product T := + eval hnf in T. + +Ltac args_unfold_head_if_not_product args := + match args with (@boxer ?T ?t)::?vs => + let T' := unfold_head_until_product T in + constr:((@boxer T' t)::vs) + end. + +Ltac args_unfold_head_if_not_product_but_params args := + match args with + | (boxer ?t)::(boxer ?v)::?vs => + args_unfold_head_if_not_product args + | _ => constr:(args) + end. + +(** [lets H: (>> E0 E1 .. EN)] will instantiate lemma [E0] + on the arguments [Ei] (which may be wildcards [__]), + and name [H] the resulting term. [H] may be an introduction + pattern, or a sequence of introduction patterns [I1 I2 IN], + or empty. + Syntax [lets H: E0 E1 .. EN] is also available. If the last + argument [EN] is [___] (triple-underscore), then all + arguments of [H] will be instantiated. *) + +Ltac lets_build I Ei := + let args := list_boxer_of Ei in + let args := args_unfold_head_if_not_product_but_params args in +(* let Ei''' := args_unfold_head_if_not_product Ei'' in*) + build_app args ltac:(fun R => lets_base I R). + +Tactic Notation "lets" simple_intropattern(I) ":" constr(E) := + lets_build I E. +Tactic Notation "lets" ":" constr(E) := + let H := fresh in lets H: E. +Tactic Notation "lets" ":" constr(E0) + constr(A1) := + lets: (>> E0 A1). +Tactic Notation "lets" ":" constr(E0) + constr(A1) constr(A2) := + lets: (>> E0 A1 A2). +Tactic Notation "lets" ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + lets: (>> E0 A1 A2 A3). +Tactic Notation "lets" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + lets: (>> E0 A1 A2 A3 A4). +Tactic Notation "lets" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + lets: (>> E0 A1 A2 A3 A4 A5). + +(* --todo: deprecated, do not use *) +Tactic Notation "lets" simple_intropattern(I1) simple_intropattern(I2) + ":" constr(E) := + lets [I1 I2]: E. +Tactic Notation "lets" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) ":" constr(E) := + lets [I1 [I2 I3]]: E. +Tactic Notation "lets" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) ":" constr(E) := + lets [I1 [I2 [I3 I4]]]: E. +Tactic Notation "lets" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) + ":" constr(E) := + lets [I1 [I2 [I3 [I4 I5]]]]: E. + +Tactic Notation "lets" simple_intropattern(I) ":" constr(E0) + constr(A1) := + lets I: (>> E0 A1). +Tactic Notation "lets" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) := + lets I: (>> E0 A1 A2). +Tactic Notation "lets" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + lets I: (>> E0 A1 A2 A3). +Tactic Notation "lets" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + lets I: (>> E0 A1 A2 A3 A4). +Tactic Notation "lets" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + lets I: (>> E0 A1 A2 A3 A4 A5). + +Tactic Notation "lets" simple_intropattern(I1) simple_intropattern(I2) ":" constr(E0) + constr(A1) := + lets [I1 I2]: E0 A1. +Tactic Notation "lets" simple_intropattern(I1) simple_intropattern(I2) ":" constr(E0) + constr(A1) constr(A2) := + lets [I1 I2]: E0 A1 A2. +Tactic Notation "lets" simple_intropattern(I1) simple_intropattern(I2) ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + lets [I1 I2]: E0 A1 A2 A3. +Tactic Notation "lets" simple_intropattern(I1) simple_intropattern(I2) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + lets [I1 I2]: E0 A1 A2 A3 A4. +Tactic Notation "lets" simple_intropattern(I1) simple_intropattern(I2) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + lets [I1 I2]: E0 A1 A2 A3 A4 A5. + + +(** [forwards H: (>> E0 E1 .. EN)] is short for + [forwards H: (>> E0 E1 .. EN ___)]. + The arguments [Ei] can be wildcards [__] (except [E0]). + [H] may be an introduction pattern, or a sequence of + introduction pattern, or empty. + Syntax [forwards H: E0 E1 .. EN] is also available. *) + +Ltac forwards_build_app_arg Ei := + let args := list_boxer_of Ei in + let args := (eval simpl in (args ++ ((boxer ___)::nil))) in + let args := args_unfold_head_if_not_product args in + args. + +Ltac forwards_then Ei cont := + let args := forwards_build_app_arg Ei in + let args := args_unfold_head_if_not_product_but_params args in + build_app args cont. + +Tactic Notation "forwards" simple_intropattern(I) ":" constr(Ei) := + let args := forwards_build_app_arg Ei in + lets I: args. + +Tactic Notation "forwards" ":" constr(E) := + let H := fresh in forwards H: E. +Tactic Notation "forwards" ":" constr(E0) + constr(A1) := + forwards: (>> E0 A1). +Tactic Notation "forwards" ":" constr(E0) + constr(A1) constr(A2) := + forwards: (>> E0 A1 A2). +Tactic Notation "forwards" ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + forwards: (>> E0 A1 A2 A3). +Tactic Notation "forwards" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + forwards: (>> E0 A1 A2 A3 A4). +Tactic Notation "forwards" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + forwards: (>> E0 A1 A2 A3 A4 A5). + +(* todo: deprecated, do not use *) +Tactic Notation "forwards" simple_intropattern(I1) simple_intropattern(I2) + ":" constr(E) := + forwards [I1 I2]: E. +Tactic Notation "forwards" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) ":" constr(E) := + forwards [I1 [I2 I3]]: E. +Tactic Notation "forwards" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) ":" constr(E) := + forwards [I1 [I2 [I3 I4]]]: E. +Tactic Notation "forwards" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) + ":" constr(E) := + forwards [I1 [I2 [I3 [I4 I5]]]]: E. + +Tactic Notation "forwards" simple_intropattern(I) ":" constr(E0) + constr(A1) := + forwards I: (>> E0 A1). +Tactic Notation "forwards" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) := + forwards I: (>> E0 A1 A2). +Tactic Notation "forwards" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + forwards I: (>> E0 A1 A2 A3). +Tactic Notation "forwards" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + forwards I: (>> E0 A1 A2 A3 A4). +Tactic Notation "forwards" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + forwards I: (>> E0 A1 A2 A3 A4 A5). + + (* for use by tactics -- todo: factorize better *) +Tactic Notation "forwards_nounfold" simple_intropattern(I) ":" constr(Ei) := + let args := list_boxer_of Ei in + let args := (eval simpl in (args ++ ((boxer ___)::nil))) in + build_app args ltac:(fun R => lets_base I R). + +Ltac forwards_nounfold_then Ei cont := + let args := list_boxer_of Ei in + let args := (eval simpl in (args ++ ((boxer ___)::nil))) in + build_app args cont. + +(** [applys (>> E0 E1 .. EN)] instantiates lemma [E0] + on the arguments [Ei] (which may be wildcards [__]), + and apply the resulting term to the current goal, + using the tactic [applys] defined earlier on. + [applys E0 E1 E2 .. EN] is also available. *) + +Ltac applys_build Ei := + let args := list_boxer_of Ei in + let args := args_unfold_head_if_not_product_but_params args in + build_app args ltac:(fun R => + first [ apply R | eapply R | rapply R ]). + +Ltac applys_base E := + match type of E with + | list Boxer => applys_build E + | _ => first [ rapply E | applys_build E ] + end; fast_rm_inside E. + +Tactic Notation "applys" constr(E) := + applys_base E. +Tactic Notation "applys" constr(E0) constr(A1) := + applys (>> E0 A1). +Tactic Notation "applys" constr(E0) constr(A1) constr(A2) := + applys (>> E0 A1 A2). +Tactic Notation "applys" constr(E0) constr(A1) constr(A2) constr(A3) := + applys (>> E0 A1 A2 A3). +Tactic Notation "applys" constr(E0) constr(A1) constr(A2) constr(A3) constr(A4) := + applys (>> E0 A1 A2 A3 A4). +Tactic Notation "applys" constr(E0) constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + applys (>> E0 A1 A2 A3 A4 A5). + +(** [fapplys (>> E0 E1 .. EN)] instantiates lemma [E0] + on the arguments [Ei] and on the argument [___] meaning + that all evars should be explicitly instantiated, + and apply the resulting term to the current goal. + [fapplys E0 E1 E2 .. EN] is also available. *) + +Ltac fapplys_build Ei := + let args := list_boxer_of Ei in + let args := (eval simpl in (args ++ ((boxer ___)::nil))) in + let args := args_unfold_head_if_not_product_but_params args in + build_app args ltac:(fun R => apply R). + +Tactic Notation "fapplys" constr(E0) := (* todo: use the tactic for that*) + match type of E0 with + | list Boxer => fapplys_build E0 + | _ => fapplys_build (>> E0) + end. +Tactic Notation "fapplys" constr(E0) constr(A1) := + fapplys (>> E0 A1). +Tactic Notation "fapplys" constr(E0) constr(A1) constr(A2) := + fapplys (>> E0 A1 A2). +Tactic Notation "fapplys" constr(E0) constr(A1) constr(A2) constr(A3) := + fapplys (>> E0 A1 A2 A3). +Tactic Notation "fapplys" constr(E0) constr(A1) constr(A2) constr(A3) constr(A4) := + fapplys (>> E0 A1 A2 A3 A4). +Tactic Notation "fapplys" constr(E0) constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + fapplys (>> E0 A1 A2 A3 A4 A5). + +(** [specializes H (>> E1 E2 .. EN)] will instantiate hypothesis [H] + on the arguments [Ei] (which may be wildcards [__]). If the last + argument [EN] is [___] (triple-underscore), then all arguments of + [H] get instantiated. *) + +Ltac specializes_build H Ei := + let H' := fresh "TEMP" in rename H into H'; + let args := list_boxer_of Ei in + let args := constr:((boxer H')::args) in + let args := args_unfold_head_if_not_product args in + build_app args ltac:(fun R => lets H: R); + clear H'. + +Ltac specializes_base H Ei := + specializes_build H Ei; fast_rm_inside Ei. + +Tactic Notation "specializes" hyp(H) := + specializes_base H (___). +Tactic Notation "specializes" hyp(H) constr(A) := + specializes_base H A. +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) := + specializes H (>> A1 A2). +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) constr(A3) := + specializes H (>> A1 A2 A3). +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) constr(A3) constr(A4) := + specializes H (>> A1 A2 A3 A4). +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + specializes H (>> A1 A2 A3 A4 A5). + +(** [specializes_vars H] is equivalent to [specializes H __ .. __] + with as many double underscore as the number of dependent arguments + visible from the type of [H]. Note that no unfolding is currently + being performed (this behavior might change in the future). + The current implementation is restricted to the case where + [H] is an existing hypothesis -- TODO: generalize. *) + +Ltac specializes_var_base H := + match type of H with + | ?P -> ?Q => fail 1 + | forall _:_, _ => specializes H __ + end. + +Ltac specializes_vars_base H := + repeat (specializes_var_base H). + +Tactic Notation "specializes_var" hyp(H) := + specializes_var_base H. + +Tactic Notation "specializes_vars" hyp(H) := + specializes_vars_base H. + +(* ---------------------------------------------------------------------- *) +(** ** Experimental tactics for application *) + +(** [fapply] is a version of [apply] based on [forwards]. *) + +Tactic Notation "fapply" constr(E) := + let H := fresh in forwards H: E; + first [ apply H | eapply H | rapply H | hnf; apply H + | hnf; eapply H | applys H ]. + (* todo: is applys redundant with rapply ? *) + +(** [sapply] stands for "super apply". It tries + [apply], [eapply], [applys] and [fapply], + and also tries to head-normalize the goal first. *) + +Tactic Notation "sapply" constr(H) := + first [ apply H | eapply H | rapply H | applys H + | hnf; apply H | hnf; eapply H | hnf; applys H + | fapply H ]. + +(* ---------------------------------------------------------------------- *) +(** ** Adding assumptions *) + +(** [lets_simpl H: E] is the same as [lets H: E] excepts that it + calls [simpl] on the hypothesis H. + [lets_simpl: E] is also provided. *) + +Tactic Notation "lets_simpl" ident(H) ":" constr(E) := + lets H: E; try simpl in H. + +Tactic Notation "lets_simpl" ":" constr(T) := + let H := fresh in lets_simpl H: T. + +(** [lets_hnf H: E] is the same as [lets H: E] excepts that it + calls [hnf] to set the definition in head normal form. + [lets_hnf: E] is also provided. *) + +Tactic Notation "lets_hnf" ident(H) ":" constr(E) := + lets H: E; hnf in H. + +Tactic Notation "lets_hnf" ":" constr(T) := + let H := fresh in lets_hnf H: T. + +(** [puts X: E] is a synonymous for [pose (X := E)]. + Alternative syntax is [puts: E]. *) + +Tactic Notation "puts" ident(X) ":" constr(E) := + pose (X := E). +Tactic Notation "puts" ":" constr(E) := + let X := fresh "X" in pose (X := E). + + +(* ---------------------------------------------------------------------- *) +(** ** Application of tautologies *) + +(** [logic E], where [E] is a fact, is equivalent to + [assert H:E; [tauto | eapply H; clear H]. It is useful for instance + to prove a conjunction [A /\ B] by showing first [A] and then [A -> B], + through the command [logic (foral A B, A -> (A -> B) -> A /\ B)] *) + +Ltac logic_base E cont := + assert (H:E); [ cont tt | eapply H; clear H ]. + +Tactic Notation "logic" constr(E) := + logic_base E ltac:(fun _ => tauto). + + +(* ---------------------------------------------------------------------- *) +(** ** Application modulo equalities *) + +(** The tactic [equates] replaces a goal of the form + [P x y z] with a goal of the form [P x ?a z] and a + subgoal [?a = y]. The introduction of the evar [?a] makes + it possible to apply lemmas that would not apply to the + original goal, for example a lemma of the form + [forall n m, P n n m], because [x] and [y] might be equal + but not convertible. + + Usage is [equates i1 ... ik], where the indices are the + positions of the arguments to be replaced by evars, + counting from the right-hand side. If [0] is given as + argument, then the entire goal is replaced by an evar. *) + +Section equatesLemma. +Variables (A0 A1 : Type). +Variables (A2 : forall (x1 : A1), Type). +Variables (A3 : forall (x1 : A1) (x2 : A2 x1), Type). +Variables (A4 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2), Type). +Variables (A5 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2) (x4 : A4 x3), Type). +Variables (A6 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2) (x4 : A4 x3) (x5 : A5 x4), Type). + +Lemma equates_0 : forall (P Q:Prop), + P -> P = Q -> Q. +Proof. intros. subst. auto. Qed. + +Lemma equates_1 : + forall (P:A0->Prop) x1 y1, + P y1 -> x1 = y1 -> P x1. +Proof. intros. subst. auto. Qed. + +Lemma equates_2 : + forall y1 (P:A0->forall(x1:A1),Prop) x1 x2, + P y1 x2 -> x1 = y1 -> P x1 x2. +Proof. intros. subst. auto. Qed. + +Lemma equates_3 : + forall y1 (P:A0->forall(x1:A1)(x2:A2 x1),Prop) x1 x2 x3, + P y1 x2 x3 -> x1 = y1 -> P x1 x2 x3. +Proof. intros. subst. auto. Qed. + +Lemma equates_4 : + forall y1 (P:A0->forall(x1:A1)(x2:A2 x1)(x3:A3 x2),Prop) x1 x2 x3 x4, + P y1 x2 x3 x4 -> x1 = y1 -> P x1 x2 x3 x4. +Proof. intros. subst. auto. Qed. + +Lemma equates_5 : + forall y1 (P:A0->forall(x1:A1)(x2:A2 x1)(x3:A3 x2)(x4:A4 x3),Prop) x1 x2 x3 x4 x5, + P y1 x2 x3 x4 x5 -> x1 = y1 -> P x1 x2 x3 x4 x5. +Proof. intros. subst. auto. Qed. + +Lemma equates_6 : + forall y1 (P:A0->forall(x1:A1)(x2:A2 x1)(x3:A3 x2)(x4:A4 x3)(x5:A5 x4),Prop) + x1 x2 x3 x4 x5 x6, + P y1 x2 x3 x4 x5 x6 -> x1 = y1 -> P x1 x2 x3 x4 x5 x6. +Proof. intros. subst. auto. Qed. + +End equatesLemma. + +Ltac equates_lemma n := + match nat_from_number n with + | 0 => constr:(equates_0) + | 1 => constr:(equates_1) + | 2 => constr:(equates_2) + | 3 => constr:(equates_3) + | 4 => constr:(equates_4) + | 5 => constr:(equates_5) + | 6 => constr:(equates_6) + end. + +Ltac equates_one n := + let L := equates_lemma n in + eapply L. + +Ltac equates_several E cont := + let all_pos := match type of E with + | List.list Boxer => constr:(E) + | _ => constr:((boxer E)::nil) + end in + let rec go pos := + match pos with + | nil => cont tt + | (boxer ?n)::?pos' => equates_one n; [ instantiate; go pos' | ] + end in + go all_pos. + +Tactic Notation "equates" constr(E) := + equates_several E ltac:(fun _ => idtac). +Tactic Notation "equates" constr(n1) constr(n2) := + equates (>> n1 n2). +Tactic Notation "equates" constr(n1) constr(n2) constr(n3) := + equates (>> n1 n2 n3). +Tactic Notation "equates" constr(n1) constr(n2) constr(n3) constr(n4) := + equates (>> n1 n2 n3 n4). + +(** [applys_eq H i1 .. iK] is the same as + [equates i1 .. iK] followed by [apply H] + on the first subgoal. *) + +Tactic Notation "applys_eq" constr(H) constr(E) := + equates_several E ltac:(fun _ => sapply H). +Tactic Notation "applys_eq" constr(H) constr(n1) constr(n2) := + applys_eq H (>> n1 n2). +Tactic Notation "applys_eq" constr(H) constr(n1) constr(n2) constr(n3) := + applys_eq H (>> n1 n2 n3). +Tactic Notation "applys_eq" constr(H) constr(n1) constr(n2) constr(n3) constr(n4) := + applys_eq H (>> n1 n2 n3 n4). + + +(* ---------------------------------------------------------------------- *) +(** ** Absurd goals *) + +(** [false_goal] replaces any goal by the goal [False]. + Contrary to the tactic [false] (below), it does not try to do + anything else *) + +Tactic Notation "false_goal" := + elimtype False. + +(** [false_post] is the underlying tactic used to prove goals + of the form [False]. In the default implementation, it proves + the goal if the context contains [False] or an hypothesis of the + form [C x1 .. xN = D y1 .. yM], or if the [congruence] tactic + finds a proof of [x <> x] for some [x]. *) + +Ltac false_post := + solve [ assumption | discriminate | congruence ]. + +(** [false] replaces any goal by the goal [False], and calls [false_post] *) + +Tactic Notation "false" := + false_goal; try false_post. + +(** [tryfalse] tries to solve a goal by contradiction, and leaves + the goal unchanged if it cannot solve it. + It is equivalent to [try solve \[ false \]]. *) + +Tactic Notation "tryfalse" := + try solve [ false ]. + +(** [false E] tries to exploit lemma [E] to prove the goal false. + [false E1 .. EN] is equivalent to [false (>> E1 .. EN)], + which tries to apply [applys (>> E1 .. EN)] and if it + does not work then tries [forwards H: (>> E1 .. EN)] + followed with [false] *) + +Ltac false_then E cont := + false_goal; first + [ applys E; instantiate + | forwards_then E ltac:(fun M => + pose M; jauto_set_hyps; intros; false) ]; + cont tt. + (* TODO: is [cont] needed? *) + +Tactic Notation "false" constr(E) := + false_then E ltac:(fun _ => idtac). +Tactic Notation "false" constr(E) constr(E1) := + false (>> E E1). +Tactic Notation "false" constr(E) constr(E1) constr(E2) := + false (>> E E1 E2). +Tactic Notation "false" constr(E) constr(E1) constr(E2) constr(E3) := + false (>> E E1 E2 E3). +Tactic Notation "false" constr(E) constr(E1) constr(E2) constr(E3) constr(E4) := + false (>> E E1 E2 E3 E4). + +(** [false_invert H] proves a goal if it absurd after + calling [inversion H] and [false] *) + +Ltac false_invert_for H := + let M := fresh in pose (M := H); inversion H; false. + +Tactic Notation "false_invert" constr(H) := + try solve [ false_invert_for H | false ]. + +(** [false_invert] proves any goal provided there is at least + one hypothesis [H] in the context (or as a universally quantified + hypothesis visible at the head of the goal) that can be proved absurd by calling + [inversion H]. *) + +Ltac false_invert_iter := + match goal with H:_ |- _ => + solve [ inversion H; false + | clear H; false_invert_iter + | fail 2 ] end. + +Tactic Notation "false_invert" := + intros; solve [ false_invert_iter | false ]. + +(** [tryfalse_invert H] and [tryfalse_invert] are like the + above but leave the goal unchanged if they don't solve it. *) + +Tactic Notation "tryfalse_invert" constr(H) := + try (false_invert H). + +Tactic Notation "tryfalse_invert" := + try false_invert. + +(** [false_neq_self_hyp] proves any goal if the context + contains an hypothesis of the form [E <> E]. It is + a restricted and optimized version of [false]. It is + intended to be used by other tactics only. *) + +Ltac false_neq_self_hyp := + match goal with H: ?x <> ?x |- _ => + false_goal; apply H; reflexivity end. + + + +(* ********************************************************************** *) +(** * Introduction and generalization *) + +(* ---------------------------------------------------------------------- *) +(** ** Introduction *) + +(** [introv] is used to name only non-dependent hypothesis. + - If [introv] is called on a goal of the form [forall x, H], + it should introduce all the variables quantified with a + [forall] at the head of the goal, but it does not introduce + hypotheses that preceed an arrow constructor, like in [P -> Q]. + - If [introv] is called on a goal that is not of the form + [forall x, H] nor [P -> Q], the tactic unfolds definitions + until the goal takes the form [forall x, H] or [P -> Q]. + If unfolding definitions does not produces a goal of this form, + then the tactic [introv] does nothing at all. *) + +(* [introv_rec] introduces all visible variables. + It does not try to unfold any definition. *) + +Ltac introv_rec := + match goal with + | |- ?P -> ?Q => idtac + | |- forall _, _ => intro; introv_rec + | |- _ => idtac + end. + +(* [introv_noarg] forces the goal to be a [forall] or an [->], + and then calls [introv_rec] to introduces variables + (possibly none, in which case [introv] is the same as [hnf]). + If the goal is not a product, then it does not do anything. *) + +Ltac introv_noarg := + match goal with + | |- ?P -> ?Q => idtac + | |- forall _, _ => introv_rec + | |- ?G => hnf; + match goal with + | |- ?P -> ?Q => idtac + | |- forall _, _ => introv_rec + end + | |- _ => idtac + end. + + (* simpler yet perhaps less efficient imlementation *) + Ltac introv_noarg_not_optimized := + intro; match goal with H:_|-_ => revert H end; introv_rec. + +(* [introv_arg H] introduces one non-dependent hypothesis + under the name [H], after introducing the variables + quantified with a [forall] that preceeds this hypothesis. + This tactic fails if there does not exist a hypothesis + to be introduced. *) + (* todo: __ in introv means "intros" *) + +Ltac introv_arg H := + hnf; match goal with + | |- ?P -> ?Q => intros H + | |- forall _, _ => intro; introv_arg H + end. + +(* [introv I1 .. IN] iterates [introv Ik] *) + +Tactic Notation "introv" := + introv_noarg. +Tactic Notation "introv" simple_intropattern(I1) := + introv_arg I1. +Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) := + introv I1; introv I2. +Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) := + introv I1; introv I2 I3. +Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) := + introv I1; introv I2 I3 I4. +Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := + introv I1; introv I2 I3 I4 I5. +Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) + simple_intropattern(I6) := + introv I1; introv I2 I3 I4 I5 I6. +Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) + simple_intropattern(I6) simple_intropattern(I7) := + introv I1; introv I2 I3 I4 I5 I6 I7. +Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) + simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) := + introv I1; introv I2 I3 I4 I5 I6 I7 I8. +Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) + simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) + simple_intropattern(I9) := + introv I1; introv I2 I3 I4 I5 I6 I7 I8 I9. +Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) + simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) + simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) + simple_intropattern(I9) simple_intropattern(I10) := + introv I1; introv I2 I3 I4 I5 I6 I7 I8 I9 I10. + +(** [intros_all] repeats [intro] as long as possible. Contrary to [intros], + it unfolds any definition on the way. Remark that it also unfolds the + definition of negation, so applying [introz] to a goal of the form + [forall x, P x -> ~Q] will introduce [x] and [P x] and [Q], and will + leave [False] in the goal. *) + +Tactic Notation "intros_all" := + repeat intro. + +(** [intros_hnf] introduces an hypothesis and sets in head normal form *) + +Tactic Notation "intro_hnf" := + intro; match goal with H: _ |- _ => hnf in H end. + + + +(* ---------------------------------------------------------------------- *) +(** ** Generalization *) + +(** [gen X1 .. XN] is a shorthand for calling [generalize dependent] + successively on variables [XN]...[X1]. Note that the variables + are generalized in reverse order, following the convention of + the [generalize] tactic: it means that [X1] will be the first + quantified variable in the resulting goal. *) + +Tactic Notation "gen" ident(X1) := + generalize dependent X1. +Tactic Notation "gen" ident(X1) ident(X2) := + gen X2; gen X1. +Tactic Notation "gen" ident(X1) ident(X2) ident(X3) := + gen X3; gen X2; gen X1. +Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) := + gen X4; gen X3; gen X2; gen X1. +Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) := + gen X5; gen X4; gen X3; gen X2; gen X1. +Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) + ident(X6) := + gen X6; gen X5; gen X4; gen X3; gen X2; gen X1. +Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) + ident(X6) ident(X7) := + gen X7; gen X6; gen X5; gen X4; gen X3; gen X2; gen X1. +Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) + ident(X6) ident(X7) ident(X8) := + gen X8; gen X7; gen X6; gen X5; gen X4; gen X3; gen X2; gen X1. +Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) + ident(X6) ident(X7) ident(X8) ident(X9) := + gen X9; gen X8; gen X7; gen X6; gen X5; gen X4; gen X3; gen X2; gen X1. +Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) + ident(X6) ident(X7) ident(X8) ident(X9) ident(X10) := + gen X10; gen X9; gen X8; gen X7; gen X6; gen X5; gen X4; gen X3; gen X2; gen X1. + +(** [generalizes X] is a shorthand for calling [generalize X; clear X]. + It is weaker than tactic [gen X] since it does not support + dependencies. It is mainly intended for writing tactics. *) + +Tactic Notation "generalizes" hyp(X) := + generalize X; clear X. +Tactic Notation "generalizes" hyp(X1) hyp(X2) := + generalizes X1; generalizes X2. +Tactic Notation "generalizes" hyp(X1) hyp(X2) hyp(X3) := + generalizes X1 X2; generalizes X3. +Tactic Notation "generalizes" hyp(X1) hyp(X2) hyp(X3) hyp(X4) := + generalizes X1 X2 X3; generalizes X4. + + +(* ---------------------------------------------------------------------- *) +(** ** Naming *) + +(** [sets X: E] is the same as [set (X := E) in *], that is, + it replaces all occurences of [E] by a fresh meta-variable [X] + whose definition is [E]. *) + +Tactic Notation "sets" ident(X) ":" constr(E) := + set (X := E) in *. + +(** [def_to_eq E X H] applies when [X := E] is a local + definition. It adds an assumption [H: X = E] + and then clears the definition of [X]. + [def_to_eq_sym] is similar except that it generates + the equality [H: E = X]. *) + +Ltac def_to_eq X HX E := + assert (HX : X = E) by reflexivity; clearbody X. +Ltac def_to_eq_sym X HX E := + assert (HX : E = X) by reflexivity; clearbody X. + +(** [set_eq X H: E] generates the equality [H: X = E], + for a fresh name [X], and replaces [E] by [X] in the + current goal. Syntaxes [set_eq X: E] and + [set_eq: E] are also available. Similarly, + [set_eq <- X H: E] generates the equality [H: E = X]. + + [sets_eq X HX: E] does the same but replaces [E] by [X] + everywhere in the goal. [sets_eq X HX: E in H] replaces in [H]. + [set_eq X HX: E in |-] performs no substitution at all. *) + +Tactic Notation "set_eq" ident(X) ident(HX) ":" constr(E) := + set (X := E); def_to_eq X HX E. +Tactic Notation "set_eq" ident(X) ":" constr(E) := + let HX := fresh "EQ" X in set_eq X HX: E. +Tactic Notation "set_eq" ":" constr(E) := + let X := fresh "X" in set_eq X: E. + +Tactic Notation "set_eq" "<-" ident(X) ident(HX) ":" constr(E) := + set (X := E); def_to_eq_sym X HX E. +Tactic Notation "set_eq" "<-" ident(X) ":" constr(E) := + let HX := fresh "EQ" X in set_eq <- X HX: E. +Tactic Notation "set_eq" "<-" ":" constr(E) := + let X := fresh "X" in set_eq <- X: E. + +Tactic Notation "sets_eq" ident(X) ident(HX) ":" constr(E) := + set (X := E) in *; def_to_eq X HX E. +Tactic Notation "sets_eq" ident(X) ":" constr(E) := + let HX := fresh "EQ" X in sets_eq X HX: E. +Tactic Notation "sets_eq" ":" constr(E) := + let X := fresh "X" in sets_eq X: E. + +Tactic Notation "sets_eq" "<-" ident(X) ident(HX) ":" constr(E) := + set (X := E) in *; def_to_eq_sym X HX E. +Tactic Notation "sets_eq" "<-" ident(X) ":" constr(E) := + let HX := fresh "EQ" X in sets_eq <- X HX: E. +Tactic Notation "sets_eq" "<-" ":" constr(E) := + let X := fresh "X" in sets_eq <- X: E. + +Tactic Notation "set_eq" ident(X) ident(HX) ":" constr(E) "in" hyp(H) := + set (X := E) in H; def_to_eq X HX E. +Tactic Notation "set_eq" ident(X) ":" constr(E) "in" hyp(H) := + let HX := fresh "EQ" X in set_eq X HX: E in H. +Tactic Notation "set_eq" ":" constr(E) "in" hyp(H) := + let X := fresh "X" in set_eq X: E in H. + +Tactic Notation "set_eq" "<-" ident(X) ident(HX) ":" constr(E) "in" hyp(H) := + set (X := E) in H; def_to_eq_sym X HX E. +Tactic Notation "set_eq" "<-" ident(X) ":" constr(E) "in" hyp(H) := + let HX := fresh "EQ" X in set_eq <- X HX: E in H. +Tactic Notation "set_eq" "<-" ":" constr(E) "in" hyp(H) := + let X := fresh "X" in set_eq <- X: E in H. + +Tactic Notation "set_eq" ident(X) ident(HX) ":" constr(E) "in" "|-" := + set (X := E) in |-; def_to_eq X HX E. +Tactic Notation "set_eq" ident(X) ":" constr(E) "in" "|-" := + let HX := fresh "EQ" X in set_eq X HX: E in |-. +Tactic Notation "set_eq" ":" constr(E) "in" "|-" := + let X := fresh "X" in set_eq X: E in |-. + +Tactic Notation "set_eq" "<-" ident(X) ident(HX) ":" constr(E) "in" "|-" := + set (X := E) in |-; def_to_eq_sym X HX E. +Tactic Notation "set_eq" "<-" ident(X) ":" constr(E) "in" "|-" := + let HX := fresh "EQ" X in set_eq <- X HX: E in |-. +Tactic Notation "set_eq" "<-" ":" constr(E) "in" "|-" := + let X := fresh "X" in set_eq <- X: E in |-. + +(** [gen_eq X: E] is a tactic whose purpose is to introduce + equalities so as to work around the limitation of the [induction] + tactic which typically loses information. [gen_eq E as X] replaces + all occurences of term [E] with a fresh variable [X] and the equality + [X = E] as extra hypothesis to the current conclusion. In other words + a conclusion [C] will be turned into [(X = E) -> C]. + [gen_eq: E] and [gen_eq: E as X] are also accepted. *) + +Tactic Notation "gen_eq" ident(X) ":" constr(E) := + let EQ := fresh in sets_eq X EQ: E; revert EQ. +Tactic Notation "gen_eq" ":" constr(E) := + let X := fresh "X" in gen_eq X: E. +Tactic Notation "gen_eq" ":" constr(E) "as" ident(X) := + gen_eq X: E. +Tactic Notation "gen_eq" ident(X1) ":" constr(E1) "," + ident(X2) ":" constr(E2) := + gen_eq X2: E2; gen_eq X1: E1. +Tactic Notation "gen_eq" ident(X1) ":" constr(E1) "," + ident(X2) ":" constr(E2) "," ident(X3) ":" constr(E3) := + gen_eq X3: E3; gen_eq X2: E2; gen_eq X1: E1. + +(** [sets_let X] finds the first let-expression in the goal + and names its body [X]. [sets_eq_let X] is similar, + except that it generates an explicit equality. + Tactics [sets_let X in H] and [sets_eq_let X in H] + allow specifying a particular hypothesis (by default, + the first one that contains a [let] is considered). + + Known limitation: it does not seem possible to support + naming of multiple let-in constructs inside a term, from ltac. *) + +Ltac sets_let_base tac := + match goal with + | |- context[let _ := ?E in _] => tac E; cbv zeta + | H: context[let _ := ?E in _] |- _ => tac E; cbv zeta in H + end. + +Ltac sets_let_in_base H tac := + match type of H with context[let _ := ?E in _] => + tac E; cbv zeta in H end. + +Tactic Notation "sets_let" ident(X) := + sets_let_base ltac:(fun E => sets X: E). +Tactic Notation "sets_let" ident(X) "in" hyp(H) := + sets_let_in_base H ltac:(fun E => sets X: E). +Tactic Notation "sets_eq_let" ident(X) := + sets_let_base ltac:(fun E => sets_eq X: E). +Tactic Notation "sets_eq_let" ident(X) "in" hyp(H) := + sets_let_in_base H ltac:(fun E => sets_eq X: E). + + +(* ********************************************************************** *) +(** * Rewriting *) + +(** [rewrites E] is similar to [rewrite] except that + it supports the [rm] directives to clear hypotheses + on the fly, and that it supports a list of arguments in the form + [rewrites (>> E1 E2 E3)] to indicate that [forwards] should be + invoked first before [rewrites] is called. *) + +Ltac rewrites_base E cont := + match type of E with + | List.list Boxer => forwards_then E cont + | _ => cont E; fast_rm_inside E + end. + +Tactic Notation "rewrites" constr(E) := + rewrites_base E ltac:(fun M => rewrite M ). +Tactic Notation "rewrites" constr(E) "in" hyp(H) := + rewrites_base E ltac:(fun M => rewrite M in H). +Tactic Notation "rewrites" constr(E) "in" "*" := + rewrites_base E ltac:(fun M => rewrite M in *). +Tactic Notation "rewrites" "<-" constr(E) := + rewrites_base E ltac:(fun M => rewrite <- M ). +Tactic Notation "rewrites" "<-" constr(E) "in" hyp(H) := + rewrites_base E ltac:(fun M => rewrite <- M in H). +Tactic Notation "rewrites" "<-" constr(E) "in" "*" := + rewrites_base E ltac:(fun M => rewrite <- M in *). + +(* TODO: extend tactics below to use [rewrites] *) + +(** [rewrite_all E] iterates version of [rewrite E] as long as possible. + Warning: this tactic can easily get into an infinite loop. + Syntax for rewriting from right to left and/or into an hypothese + is similar to the one of [rewrite]. *) + +Tactic Notation "rewrite_all" constr(E) := + repeat rewrite E. +Tactic Notation "rewrite_all" "<-" constr(E) := + repeat rewrite <- E. +Tactic Notation "rewrite_all" constr(E) "in" ident(H) := + repeat rewrite E in H. +Tactic Notation "rewrite_all" "<-" constr(E) "in" ident(H) := + repeat rewrite <- E in H. +Tactic Notation "rewrite_all" constr(E) "in" "*" := + repeat rewrite E in *. +Tactic Notation "rewrite_all" "<-" constr(E) "in" "*" := + repeat rewrite <- E in *. + +(** [asserts_rewrite E] asserts that an equality [E] holds (generating a + corresponding subgoal) and rewrite it straight away in the current + goal. It avoids giving a name to the equality and later clearing it. + Syntax for rewriting from right to left and/or into an hypothese + is similar to the one of [rewrite]. Note: the tactic [replaces] + plays a similar role. *) + +Ltac asserts_rewrite_tactic E action := + let EQ := fresh in (assert (EQ : E); + [ idtac | action EQ; clear EQ ]). + +Tactic Notation "asserts_rewrite" constr(E) := + asserts_rewrite_tactic E ltac:(fun EQ => rewrite EQ). +Tactic Notation "asserts_rewrite" "<-" constr(E) := + asserts_rewrite_tactic E ltac:(fun EQ => rewrite <- EQ). +Tactic Notation "asserts_rewrite" constr(E) "in" hyp(H) := + asserts_rewrite_tactic E ltac:(fun EQ => rewrite EQ in H). +Tactic Notation "asserts_rewrite" "<-" constr(E) "in" hyp(H) := + asserts_rewrite_tactic E ltac:(fun EQ => rewrite <- EQ in H). +Tactic Notation "asserts_rewrite" constr(E) "in" "*" := + asserts_rewrite_tactic E ltac:(fun EQ => rewrite EQ in *). +Tactic Notation "asserts_rewrite" "<-" constr(E) "in" "*" := + asserts_rewrite_tactic E ltac:(fun EQ => rewrite <- EQ in *). + +(** [cuts_rewrite E] is the same as [asserts_rewrite E] except + that subgoals are permuted. *) + +Ltac cuts_rewrite_tactic E action := + let EQ := fresh in (cuts EQ: E; + [ action EQ; clear EQ | idtac ]). + +Tactic Notation "cuts_rewrite" constr(E) := + cuts_rewrite_tactic E ltac:(fun EQ => rewrite EQ). +Tactic Notation "cuts_rewrite" "<-" constr(E) := + cuts_rewrite_tactic E ltac:(fun EQ => rewrite <- EQ). +Tactic Notation "cuts_rewrite" constr(E) "in" hyp(H) := + cuts_rewrite_tactic E ltac:(fun EQ => rewrite EQ in H). +Tactic Notation "cuts_rewrite" "<-" constr(E) "in" hyp(H) := + cuts_rewrite_tactic E ltac:(fun EQ => rewrite <- EQ in H). + +(** [rewrite_except H EQ] rewrites equality [EQ] everywhere + but in hypothesis [H]. Mainly useful for other tactics. *) + +Ltac rewrite_except H EQ := + let K := fresh in let T := type of H in + set (K := T) in H; + rewrite EQ in *; unfold K in H; clear K. + +(** [rewrites E at K] applies when [E] is of the form [T1 = T2] + rewrites the equality [E] at the [K]-th occurence of [T1] + in the current goal. + Syntaxes [rewrites <- E at K] and [rewrites E at K in H] + are also available. *) + +Tactic Notation "rewrites" constr(E) "at" constr(K) := + match type of E with ?T1 = ?T2 => + ltac_action_at K of T1 do (rewrites E) end. +Tactic Notation "rewrites" "<-" constr(E) "at" constr(K) := + match type of E with ?T1 = ?T2 => + ltac_action_at K of T2 do (rewrites <- E) end. +Tactic Notation "rewrites" constr(E) "at" constr(K) "in" hyp(H) := + match type of E with ?T1 = ?T2 => + ltac_action_at K of T1 in H do (rewrites E in H) end. +Tactic Notation "rewrites" "<-" constr(E) "at" constr(K) "in" hyp(H) := + match type of E with ?T1 = ?T2 => + ltac_action_at K of T2 in H do (rewrites <- E in H) end. + + +(* ---------------------------------------------------------------------- *) +(** ** Replace *) + +(** [replaces E with F] is the same as [replace E with F] except that + the equality [E = F] is generated as first subgoal. Syntax + [replaces E with F in H] is also available. Note that contrary to + [replace], [replaces] does not try to solve the equality + by [assumption]. Note: [replaces E with F] is similar to + [asserts_rewrite (E = F)]. *) + +Tactic Notation "replaces" constr(E) "with" constr(F) := + let T := fresh in assert (T: E = F); [ | replace E with F; clear T ]. + +Tactic Notation "replaces" constr(E) "with" constr(F) "in" hyp(H) := + let T := fresh in assert (T: E = F); [ | replace E with F in H; clear T ]. + + +(** [replaces E at K with F] replaces the [K]-th occurence of [E] + with [F] in the current goal. Syntax [replaces E at K with F in H] + is also available. *) + +Tactic Notation "replaces" constr(E) "at" constr(K) "with" constr(F) := + let T := fresh in assert (T: E = F); [ | rewrites T at K; clear T ]. + +Tactic Notation "replaces" constr(E) "at" constr(K) "with" constr(F) "in" hyp(H) := + let T := fresh in assert (T: E = F); [ | rewrites T at K in H; clear T ]. + + +(* ---------------------------------------------------------------------- *) +(** ** Change *) + +(** [changes] is like [change] except that it does not silently + fail to perform its task. (Note that, [changes] is implemented + using [rewrite], meaning that it might perform additional + beta-reductions compared with the original [change] tactic. *) +(* TODO: support "changes (E1 = E2)" *) + +Tactic Notation "changes" constr(E1) "with" constr(E2) "in" hyp(H) := + asserts_rewrite (E1 = E2) in H; [ reflexivity | ]. + +Tactic Notation "changes" constr(E1) "with" constr(E2) := + asserts_rewrite (E1 = E2); [ reflexivity | ]. + +Tactic Notation "changes" constr(E1) "with" constr(E2) "in" "*" := + asserts_rewrite (E1 = E2) in *; [ reflexivity | ]. + + + +(* ---------------------------------------------------------------------- *) +(** ** Renaming *) + +(** [renames X1 to Y1, ..., XN to YN] is a shorthand for a sequence of + renaming operations [rename Xi into Yi]. *) + +Tactic Notation "renames" ident(X1) "to" ident(Y1) := + rename X1 into Y1. +Tactic Notation "renames" ident(X1) "to" ident(Y1) "," + ident(X2) "to" ident(Y2) := + renames X1 to Y1; renames X2 to Y2. +Tactic Notation "renames" ident(X1) "to" ident(Y1) "," + ident(X2) "to" ident(Y2) "," ident(X3) "to" ident(Y3) := + renames X1 to Y1; renames X2 to Y2, X3 to Y3. +Tactic Notation "renames" ident(X1) "to" ident(Y1) "," + ident(X2) "to" ident(Y2) "," ident(X3) "to" ident(Y3) "," + ident(X4) "to" ident(Y4) := + renames X1 to Y1; renames X2 to Y2, X3 to Y3, X4 to Y4. +Tactic Notation "renames" ident(X1) "to" ident(Y1) "," + ident(X2) "to" ident(Y2) "," ident(X3) "to" ident(Y3) "," + ident(X4) "to" ident(Y4) "," ident(X5) "to" ident(Y5) := + renames X1 to Y1; renames X2 to Y2, X3 to Y3, X4 to Y4, X5 to Y5. +Tactic Notation "renames" ident(X1) "to" ident(Y1) "," + ident(X2) "to" ident(Y2) "," ident(X3) "to" ident(Y3) "," + ident(X4) "to" ident(Y4) "," ident(X5) "to" ident(Y5) "," + ident(X6) "to" ident(Y6) := + renames X1 to Y1; renames X2 to Y2, X3 to Y3, X4 to Y4, X5 to Y5, X6 to Y6. + + +(* ---------------------------------------------------------------------- *) +(** ** Unfolding *) + +(** [unfolds] unfolds the head definition in the goal, i.e., if the + goal has form [P x1 ... xN] then it calls [unfold P]. + If the goal is an equality, it tries to unfold the head constant + on the left-hand side, and otherwise tries on the right-hand side. + If the goal is a product, it calls [intros] first. + -- warning: this tactic is overriden in LibReflect. *) + +Ltac apply_to_head_of E cont := + let go E := + let P := get_head E in cont P in + match E with + | forall _,_ => intros; apply_to_head_of E cont + | ?A = ?B => first [ go A | go B ] + | ?A => go A + end. + +Ltac unfolds_base := + match goal with |- ?G => + apply_to_head_of G ltac:(fun P => unfold P) end. + +Tactic Notation "unfolds" := + unfolds_base. + +(** [unfolds in H] unfolds the head definition of hypothesis [H], i.e., if + [H] has type [P x1 ... xN] then it calls [unfold P in H]. *) + +Ltac unfolds_in_base H := + match type of H with ?G => + apply_to_head_of G ltac:(fun P => unfold P in H) end. + +Tactic Notation "unfolds" "in" hyp(H) := + unfolds_in_base H. + +(** [unfolds in H1,H2,..,HN] allows unfolding the head constant + in several hypotheses at once. *) + +Tactic Notation "unfolds" "in" hyp(H1) hyp(H2) := + unfolds in H1; unfolds in H2. +Tactic Notation "unfolds" "in" hyp(H1) hyp(H2) hyp(H3) := + unfolds in H1; unfolds in H2 H3. +Tactic Notation "unfolds" "in" hyp(H1) hyp(H2) hyp(H3) hyp(H4) := + unfolds in H1; unfolds in H2 H3 H4. + +(** [unfolds P1,..,PN] is a shortcut for [unfold P1,..,PN in *]. *) + +Tactic Notation "unfolds" constr(F1) := + unfold F1 in *. +Tactic Notation "unfolds" constr(F1) "," constr(F2) := + unfold F1,F2 in *. +Tactic Notation "unfolds" constr(F1) "," constr(F2) + "," constr(F3) := + unfold F1,F2,F3 in *. +Tactic Notation "unfolds" constr(F1) "," constr(F2) + "," constr(F3) "," constr(F4) := + unfold F1,F2,F3,F4 in *. +Tactic Notation "unfolds" constr(F1) "," constr(F2) + "," constr(F3) "," constr(F4) "," constr(F5) := + unfold F1,F2,F3,F4,F5 in *. +Tactic Notation "unfolds" constr(F1) "," constr(F2) + "," constr(F3) "," constr(F4) "," constr(F5) "," constr(F6) := + unfold F1,F2,F3,F4,F5,F6 in *. +Tactic Notation "unfolds" constr(F1) "," constr(F2) + "," constr(F3) "," constr(F4) "," constr(F5) + "," constr(F6) "," constr(F7) := + unfold F1,F2,F3,F4,F5,F6,F7 in *. +Tactic Notation "unfolds" constr(F1) "," constr(F2) + "," constr(F3) "," constr(F4) "," constr(F5) + "," constr(F6) "," constr(F7) "," constr(F8) := + unfold F1,F2,F3,F4,F5,F6,F7,F8 in *. + +(** [folds P1,..,PN] is a shortcut for [fold P1 in *; ..; fold PN in *]. *) + +Tactic Notation "folds" constr(H) := + fold H in *. +Tactic Notation "folds" constr(H1) "," constr(H2) := + folds H1; folds H2. +Tactic Notation "folds" constr(H1) "," constr(H2) "," constr(H3) := + folds H1; folds H2; folds H3. +Tactic Notation "folds" constr(H1) "," constr(H2) "," constr(H3) + "," constr(H4) := + folds H1; folds H2; folds H3; folds H4. +Tactic Notation "folds" constr(H1) "," constr(H2) "," constr(H3) + "," constr(H4) "," constr(H5) := + folds H1; folds H2; folds H3; folds H4; folds H5. + + +(* ---------------------------------------------------------------------- *) +(** ** Simplification *) + +(** [simpls] is a shortcut for [simpl in *]. *) + +Tactic Notation "simpls" := + simpl in *. + +(** [simpls P1,..,PN] is a shortcut for + [simpl P1 in *; ..; simpl PN in *]. *) + +Tactic Notation "simpls" constr(F1) := + simpl F1 in *. +Tactic Notation "simpls" constr(F1) "," constr(F2) := + simpls F1; simpls F2. +Tactic Notation "simpls" constr(F1) "," constr(F2) + "," constr(F3) := + simpls F1; simpls F2; simpls F3. +Tactic Notation "simpls" constr(F1) "," constr(F2) + "," constr(F3) "," constr(F4) := + simpls F1; simpls F2; simpls F3; simpls F4. + +(** [unsimpl E] replaces all occurence of [X] by [E], where [X] is + the result which the tactic [simpl] would give when applied to [E]. + It is useful to undo what [simpl] has simplified too far. *) + +Tactic Notation "unsimpl" constr(E) := + let F := (eval simpl in E) in change F with E. + +(** [unsimpl E in H] is similar to [unsimpl E] but it applies + inside a particular hypothesis [H]. *) + +Tactic Notation "unsimpl" constr(E) "in" hyp(H) := + let F := (eval simpl in E) in change F with E in H. + +(** [unsimpl E in *] applies [unsimpl E] everywhere possible. + [unsimpls E] is a synonymous. *) + +Tactic Notation "unsimpl" constr(E) "in" "*" := + let F := (eval simpl in E) in change F with E in *. +Tactic Notation "unsimpls" constr(E) := + unsimpl E in *. + +(** [nosimpl t] protects the Coq term[t] against some forms of + simplification. See Gonthier's work for details on this trick. *) + +Notation "'nosimpl' t" := (match tt with tt => t end) + (at level 10). + + +(* ---------------------------------------------------------------------- *) +(** ** Evaluation *) + +Tactic Notation "hnfs" := hnf in *. + +(* ---------------------------------------------------------------------- *) +(** ** Substitution *) + +(** [substs] does the same as [subst], except that it does not fail + when there are circular equalities in the context. *) + +Tactic Notation "substs" := + repeat (match goal with H: ?x = ?y |- _ => + first [ subst x | subst y ] end). + +(** Implementation of [substs below], which allows to call + [subst] on all the hypotheses that lie beyond a given + position in the proof context. *) + +Ltac substs_below limit := + match goal with H: ?T |- _ => + match T with + | limit => idtac + | ?x = ?y => + first [ subst x; substs_below limit + | subst y; substs_below limit + | generalizes H; substs_below limit; intro ] + end end. + +(** [substs below body E] applies [subst] on all equalities that appear + in the context below the first hypothesis whose body is [E]. + If there is no such hypothesis in the context, it is equivalent + to [subst]. For instance, if [H] is an hypothesis, then + [substs below H] will substitute equalities below hypothesis [H]. *) + +Tactic Notation "substs" "below" "body" constr(M) := + substs_below M. + +(** [substs below H] applies [subst] on all equalities that appear + in the context below the hypothesis named [H]. Note that + the current implementation is technically incorrect since it + will confuse different hypotheses with the same body. *) + +Tactic Notation "substs" "below" hyp(H) := + match type of H with ?M => substs below body M end. + +(** [subst_hyp H] substitutes the equality contained in the + first hypothesis from the context. *) + +Ltac intro_subst_hyp := fail. (* definition further on *) + +(** [subst_hyp H] substitutes the equality contained in [H]. *) + +Ltac subst_hyp_base H := + match type of H with + | (_,_,_,_,_) = (_,_,_,_,_) => injection H; clear H; do 4 intro_subst_hyp + | (_,_,_,_) = (_,_,_,_) => injection H; clear H; do 4 intro_subst_hyp + | (_,_,_) = (_,_,_) => injection H; clear H; do 3 intro_subst_hyp + | (_,_) = (_,_) => injection H; clear H; do 2 intro_subst_hyp + | ?x = ?x => clear H + | ?x = ?y => first [ subst x | subst y ] + end. + +Tactic Notation "subst_hyp" hyp(H) := subst_hyp_base H. + +Ltac intro_subst_hyp ::= + let H := fresh "TEMP" in intros H; subst_hyp H. + +(** [intro_subst] is a shorthand for [intro H; subst_hyp H]: + it introduces and substitutes the equality at the head + of the current goal. *) + +Tactic Notation "intro_subst" := + let H := fresh "TEMP" in intros H; subst_hyp H. + +(** [subst_local] substitutes all local definition from the context *) + +Ltac subst_local := + repeat match goal with H:=_ |- _ => subst H end. + +(** [subst_eq E] takes an equality [x = t] and replace [x] + with [t] everywhere in the goal *) + +Ltac subst_eq_base E := + let H := fresh "TEMP" in lets H: E; subst_hyp H. + +Tactic Notation "subst_eq" constr(E) := + subst_eq_base E. + + +(* ---------------------------------------------------------------------- *) +(** ** Tactics to work with proof irrelevance *) + +Require Import ProofIrrelevance. + +(** [pi_rewrite E] replaces [E] of type [Prop] with a fresh + unification variable, and is thus a practical way to + exploit proof irrelevance, without writing explicitly + [rewrite (proof_irrelevance E E')]. Particularly useful + when [E'] is a big expression. *) + +Ltac pi_rewrite_base E rewrite_tac := + let E' := fresh in let T := type of E in evar (E':T); + rewrite_tac (@proof_irrelevance _ E E'); subst E'. + +Tactic Notation "pi_rewrite" constr(E) := + pi_rewrite_base E ltac:(fun X => rewrite X). +Tactic Notation "pi_rewrite" constr(E) "in" hyp(H) := + pi_rewrite_base E ltac:(fun X => rewrite X in H). + + +(* ---------------------------------------------------------------------- *) +(** ** Proving equalities *) + +(** Note: current implementation only supports up to arity 5 *) + +(** [fequal] is a variation on [f_equal] which has a better behaviour + on equalities between n-ary tuples. *) + +Ltac fequal_base := + let go := f_equal; [ fequal_base | ] in + match goal with + | |- (_,_,_) = (_,_,_) => go + | |- (_,_,_,_) = (_,_,_,_) => go + | |- (_,_,_,_,_) = (_,_,_,_,_) => go + | |- (_,_,_,_,_,_) = (_,_,_,_,_,_) => go + | |- _ => f_equal + end. + +Tactic Notation "fequal" := + fequal_base. + +(** [fequals] is the same as [fequal] except that it tries and solve + all trivial subgoals, using [reflexivity] and [congruence] + (as well as the proof-irrelevance principle). + [fequals] applies to goals of the form [f x1 .. xN = f y1 .. yN] + and produces some subgoals of the form [xi = yi]). *) + +Ltac fequal_post := + first [ reflexivity | congruence | apply proof_irrelevance | idtac ]. + +Tactic Notation "fequals" := + fequal; fequal_post. + +(** [fequals_rec] calls [fequals] recursively. + It is equivalent to [repeat (progress fequals)]. *) + +Tactic Notation "fequals_rec" := + repeat (progress fequals). + + + +(* ********************************************************************** *) +(** * Inversion *) + +(* ---------------------------------------------------------------------- *) +(** ** Basic inversion *) + +(** [invert keep H] is same to [inversion H] except that it puts all the + facts obtained in the goal. The keyword [keep] means that the + hypothesis [H] should not be removed. *) + +Tactic Notation "invert" "keep" hyp(H) := + pose ltac_mark; inversion H; gen_until_mark. + +(** [invert keep H as X1 .. XN] is the same as [inversion H as ...] except + that only hypotheses which are not variable need to be named + explicitely, in a similar fashion as [introv] is used to name + only hypotheses. *) + +Tactic Notation "invert" "keep" hyp(H) "as" simple_intropattern(I1) := + invert keep H; introv I1. +Tactic Notation "invert" "keep" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) := + invert keep H; introv I1 I2. +Tactic Notation "invert" "keep" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) := + invert keep H; introv I1 I2 I3. + +(** [invert H] is same to [inversion H] except that it puts all the + facts obtained in the goal and clears hypothesis [H]. + In other words, it is equivalent to [invert keep H; clear H]. *) + +Tactic Notation "invert" hyp(H) := + invert keep H; clear H. + +(** [invert H as X1 .. XN] is the same as [invert keep H as X1 .. XN] + but it also clears hypothesis [H]. *) + +Tactic Notation "invert_tactic" hyp(H) tactic(tac) := + let H' := fresh in rename H into H'; tac H'; clear H'. +Tactic Notation "invert" hyp(H) "as" simple_intropattern(I1) := + invert_tactic H (fun H => invert keep H as I1). +Tactic Notation "invert" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) := + invert_tactic H (fun H => invert keep H as I1 I2). +Tactic Notation "invert" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) := + invert_tactic H (fun H => invert keep H as I1 I2 I3). + + +(* ---------------------------------------------------------------------- *) +(** ** Inversion with substitution *) + +(** Our inversion tactics is able to get rid of dependent equalities + generated by [inversion], using proof irrelevance. *) + +(* --we do not import Eqdep because it imports nasty hints automatically + Require Import Eqdep. *) + +Axiom inj_pair2 : (* is in fact derivable from the axioms in LibAxiom.v *) + forall (U : Type) (P : U -> Type) (p : U) (x y : P p), + existT P p x = existT P p y -> x = y. +(* Proof using. apply Eqdep.EqdepTheory.inj_pair2. Qed.*) + +Ltac inverts_tactic H i1 i2 i3 i4 i5 i6 := + let rec go i1 i2 i3 i4 i5 i6 := + match goal with + | |- (ltac_Mark -> _) => intros _ + | |- (?x = ?y -> _) => let H := fresh in intro H; + first [ subst x | subst y ]; + go i1 i2 i3 i4 i5 i6 + | |- (existT ?P ?p ?x = existT ?P ?p ?y -> _) => + let H := fresh in intro H; + generalize (@inj_pair2 _ P p x y H); + clear H; go i1 i2 i3 i4 i5 i6 + | |- (?P -> ?Q) => i1; go i2 i3 i4 i5 i6 ltac:(intro) + | |- (forall _, _) => intro; go i1 i2 i3 i4 i5 i6 + end in + generalize ltac_mark; invert keep H; go i1 i2 i3 i4 i5 i6; + unfold eq' in *. + +(** [inverts keep H] is same to [invert keep H] except that it + applies [subst] to all the equalities generated by the inversion. *) + +Tactic Notation "inverts" "keep" hyp(H) := + inverts_tactic H ltac:(intro) ltac:(intro) ltac:(intro) + ltac:(intro) ltac:(intro) ltac:(intro). + +(** [inverts keep H as X1 .. XN] is the same as + [invert keep H as X1 .. XN] except that it applies [subst] to all the + equalities generated by the inversion *) + +Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1) := + inverts_tactic H ltac:(intros I1) + ltac:(intro) ltac:(intro) ltac:(intro) ltac:(intro) ltac:(intro). +Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) := + inverts_tactic H ltac:(intros I1) ltac:(intros I2) + ltac:(intro) ltac:(intro) ltac:(intro) ltac:(intro). +Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) := + inverts_tactic H ltac:(intros I1) ltac:(intros I2) ltac:(intros I3) + ltac:(intro) ltac:(intro) ltac:(intro). +Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) := + inverts_tactic H ltac:(intros I1) ltac:(intros I2) ltac:(intros I3) + ltac:(intros I4) ltac:(intro) ltac:(intro). +Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) + simple_intropattern(I5) := + inverts_tactic H ltac:(intros I1) ltac:(intros I2) ltac:(intros I3) + ltac:(intros I4) ltac:(intros I5) ltac:(intro). +Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) + simple_intropattern(I5) simple_intropattern(I6) := + inverts_tactic H ltac:(intros I1) ltac:(intros I2) ltac:(intros I3) + ltac:(intros I4) ltac:(intros I5) ltac:(intros I6). + +(** [inverts H] is same to [inverts keep H] except that it + clears hypothesis [H]. *) + +Tactic Notation "inverts" hyp(H) := + inverts keep H; clear H. + +(** [inverts H as X1 .. XN] is the same as [inverts keep H as X1 .. XN] + but it also clears the hypothesis [H]. *) + +Tactic Notation "inverts_tactic" hyp(H) tactic(tac) := + let H' := fresh in rename H into H'; tac H'; clear H'. +Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1) := + invert_tactic H (fun H => inverts keep H as I1). +Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) := + invert_tactic H (fun H => inverts keep H as I1 I2). +Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) := + invert_tactic H (fun H => inverts keep H as I1 I2 I3). +Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) := + invert_tactic H (fun H => inverts keep H as I1 I2 I3 I4). +Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) + simple_intropattern(I5) := + invert_tactic H (fun H => inverts keep H as I1 I2 I3 I4 I5). +Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) + simple_intropattern(I5) simple_intropattern(I6) := + invert_tactic H (fun H => inverts keep H as I1 I2 I3 I4 I5 I6). + +(** [inverts H as] performs an inversion on hypothesis [H], substitutes + generated equalities, and put in the goal the other freshly-created + hypotheses, for the user to name explicitly. + [inverts keep H as] is the same except that it does not clear [H]. + --TODO: reimplement [inverts] above using this one *) + +Ltac inverts_as_tactic H := + let rec go tt := + match goal with + | |- (ltac_Mark -> _) => intros _ + | |- (?x = ?y -> _) => let H := fresh "TEMP" in intro H; + first [ subst x | subst y ]; + go tt + | |- (existT ?P ?p ?x = existT ?P ?p ?y -> _) => + let H := fresh in intro H; + generalize (@inj_pair2 _ P p x y H); + clear H; go tt + | |- (forall _, _) => + intro; let H := get_last_hyp tt in mark_to_generalize H; go tt + end in + pose ltac_mark; inversion H; + generalize ltac_mark; gen_until_mark; + go tt; gen_to_generalize; unfolds ltac_to_generalize; + unfold eq' in *. + +Tactic Notation "inverts" "keep" hyp(H) "as" := + inverts_as_tactic H. + +Tactic Notation "inverts" hyp(H) "as" := + inverts_as_tactic H; clear H. + +Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) + simple_intropattern(I5) simple_intropattern(I6) simple_intropattern(I7) := + inverts H as; introv I1 I2 I3 I4 I5 I6 I7. +Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) + simple_intropattern(I5) simple_intropattern(I6) simple_intropattern(I7) + simple_intropattern(I8) := + inverts H as; introv I1 I2 I3 I4 I5 I6 I7 I8. + + +(** [lets_inverts E as I1 .. IN] is intuitively equivalent to + [inverts E], with the difference that it applies to any + expression and not just to the name of an hypothesis. *) + +Ltac lets_inverts_base E cont := + let H := fresh "TEMP" in lets H: E; try cont H. + +Tactic Notation "lets_inverts" constr(E) := + lets_inverts_base E ltac:(fun H => inverts H). +Tactic Notation "lets_inverts" constr(E) "as" simple_intropattern(I1) := + lets_inverts_base E ltac:(fun H => inverts H as I1). +Tactic Notation "lets_inverts" constr(E) "as" simple_intropattern(I1) + simple_intropattern(I2) := + lets_inverts_base E ltac:(fun H => inverts H as I1 I2). +Tactic Notation "lets_inverts" constr(E) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) := + lets_inverts_base E ltac:(fun H => inverts H as I1 I2 I3). +Tactic Notation "lets_inverts" constr(E) "as" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) := + lets_inverts_base E ltac:(fun H => inverts H as I1 I2 I3 I4). + + + +(* ---------------------------------------------------------------------- *) +(** ** Injection with substitution *) + +(** Underlying implementation of [injects] *) + +Ltac injects_tactic H := + let rec go _ := + match goal with + | |- (ltac_Mark -> _) => intros _ + | |- (?x = ?y -> _) => let H := fresh in intro H; + first [ subst x | subst y | idtac ]; + go tt + end in + generalize ltac_mark; injection H; go tt. + +(** [injects keep H] takes an hypothesis [H] of the form + [C a1 .. aN = C b1 .. bN] and substitute all equalities + [ai = bi] that have been generated. *) + +Tactic Notation "injects" "keep" hyp(H) := + injects_tactic H. + +(** [injects H] is similar to [injects keep H] but clears + the hypothesis [H]. *) + +Tactic Notation "injects" hyp(H) := + injects_tactic H; clear H. + +(** [inject H as X1 .. XN] is the same as [injection] + followed by [intros X1 .. XN] *) + +Tactic Notation "inject" hyp(H) := + injection H. +Tactic Notation "inject" hyp(H) "as" ident(X1) := + injection H; intros X1. +Tactic Notation "inject" hyp(H) "as" ident(X1) ident(X2) := + injection H; intros X1 X2. +Tactic Notation "inject" hyp(H) "as" ident(X1) ident(X2) ident(X3) := + injection H; intros X1 X2 X3. +Tactic Notation "inject" hyp(H) "as" ident(X1) ident(X2) ident(X3) + ident(X4) := + injection H; intros X1 X2 X3 X4. +Tactic Notation "inject" hyp(H) "as" ident(X1) ident(X2) ident(X3) + ident(X4) ident(X5) := + injection H; intros X1 X2 X3 X4 X5. + + +(* ---------------------------------------------------------------------- *) +(** ** Inversion and injection with substitution --rough implementation *) + +(** The tactics [inversions] and [injections] provided in this section + are similar to [inverts] and [injects] except that they perform + substitution on all equalities from the context and not only + the ones freshly generated. The counterpart is that they have + simpler implementations. *) + +(** [inversions keep H] is the same as [inversions H] but it does + not clear hypothesis [H]. *) + +Tactic Notation "inversions" "keep" hyp(H) := + inversion H; subst. + +(** [inversions H] is a shortcut for [inversion H] followed by [subst] + and [clear H]. + It is a rough implementation of [inverts keep H] which behave + badly when the proof context already contains equalities. + It is provided in case the better implementation turns out to be + too slow. *) + +Tactic Notation "inversions" hyp(H) := + inversion H; subst; clear H. + +(** [injections keep H] is the same as [injection H] followed + by [intros] and [subst]. It is a rough implementation of + [injects keep H] which behave + badly when the proof context already contains equalities, + or when the goal starts with a forall or an implication. *) + +Tactic Notation "injections" "keep" hyp(H) := + injection H; intros; subst. + +(** [injections H] is the same as [injection H] followed + by [intros] and [clear H] and [subst]. It is a rough + implementation of [injects keep H] which behave + badly when the proof context already contains equalities, + or when the goal starts with a forall or an implication. *) + +Tactic Notation "injections" "keep" hyp(H) := + injection H; clear H; intros; subst. + + +(* ---------------------------------------------------------------------- *) +(** ** Case analysis *) + +(** [cases] is similar to [case_eq E] except that it generates the + equality in the context and not in the goal, and generates the + equality the other way round. The syntax [cases E as H] + allows specifying the name [H] of that hypothesis. *) + +Tactic Notation "cases" constr(E) "as" ident(H) := + let X := fresh "TEMP" in + set (X := E) in *; def_to_eq_sym X H E; + destruct X. + +Tactic Notation "cases" constr(E) := + let H := fresh "Eq" in cases E as H. + +(** [case_if_post] is to be defined later as a tactic to clean + up goals. By defaults, it looks for obvious contradictions. + Currently, this tactic is extended in LibReflect to clean up + boolean propositions. *) + +Ltac case_if_post := tryfalse. + +(** [case_if] looks for a pattern of the form [if ?B then ?E1 else ?E2] + in the goal, and perform a case analysis on [B] by calling + [destruct B]. Subgoals containing a contradiction are discarded. + [case_if] looks in the goal first, and otherwise in the + first hypothesis that contains and [if] statement. + [case_if in H] can be used to specify which hypothesis to consider. + Syntaxes [case_if as Eq] and [case_if in H as Eq] allows to name + the hypothesis coming from the case analysis. *) + +Ltac case_if_on_tactic_core E Eq := + match type of E with + | {_}+{_} => destruct E as [Eq | Eq] + | _ => let X := fresh in + sets_eq <- X Eq: E; + destruct X + end. + +Ltac case_if_on_tactic E Eq := + case_if_on_tactic_core E Eq; case_if_post. + +Tactic Notation "case_if_on" constr(E) "as" simple_intropattern(Eq) := + case_if_on_tactic E Eq. + +Tactic Notation "case_if" "as" simple_intropattern(Eq) := + match goal with + | |- context [if ?B then _ else _] => case_if_on B as Eq + | K: context [if ?B then _ else _] |- _ => case_if_on B as Eq + end. + +Tactic Notation "case_if" "in" hyp(H) "as" simple_intropattern(Eq) := + match type of H with context [if ?B then _ else _] => + case_if_on B as Eq end. + +Tactic Notation "case_if" := + let Eq := fresh in case_if as Eq. + +Tactic Notation "case_if" "in" hyp(H) := + let Eq := fresh in case_if in H as Eq. + + +(** [cases_if] is similar to [case_if] with two main differences: + if it creates an equality of the form [x = y] and then + substitutes it in the goal *) + +Ltac cases_if_on_tactic_core E Eq := + match type of E with + | {_}+{_} => destruct E as [Eq|Eq]; try subst_hyp Eq + | _ => let X := fresh in + sets_eq <- X Eq: E; + destruct X + end. + +Ltac cases_if_on_tactic E Eq := + cases_if_on_tactic_core E Eq; tryfalse; case_if_post. + +Tactic Notation "cases_if_on" constr(E) "as" simple_intropattern(Eq) := + cases_if_on_tactic E Eq. + +Tactic Notation "cases_if" "as" simple_intropattern(Eq) := + match goal with + | |- context [if ?B then _ else _] => cases_if_on B as Eq + | K: context [if ?B then _ else _] |- _ => cases_if_on B as Eq + end. + +Tactic Notation "cases_if" "in" hyp(H) "as" simple_intropattern(Eq) := + match type of H with context [if ?B then _ else _] => + cases_if_on B as Eq end. + +Tactic Notation "cases_if" := + let Eq := fresh in cases_if as Eq. + +Tactic Notation "cases_if" "in" hyp(H) := + let Eq := fresh in cases_if in H as Eq. + +(** [case_ifs] is like [repeat case_if] *) + +Ltac case_ifs_core := + repeat case_if. + +Tactic Notation "case_ifs" := + case_ifs_core. + +(** [destruct_if] looks for a pattern of the form [if ?B then ?E1 else ?E2] + in the goal, and perform a case analysis on [B] by calling + [destruct B]. It looks in the goal first, and otherwise in the + first hypothesis that contains and [if] statement. *) + +Ltac destruct_if_post := tryfalse. + +Tactic Notation "destruct_if" + "as" simple_intropattern(Eq1) simple_intropattern(Eq2) := + match goal with + | |- context [if ?B then _ else _] => destruct B as [Eq1|Eq2] + | K: context [if ?B then _ else _] |- _ => destruct B as [Eq1|Eq2] + end; + destruct_if_post. + +Tactic Notation "destruct_if" "in" hyp(H) + "as" simple_intropattern(Eq1) simple_intropattern(Eq2) := + match type of H with context [if ?B then _ else _] => + destruct B as [Eq1|Eq2] end; + destruct_if_post. + +Tactic Notation "destruct_if" "as" simple_intropattern(Eq) := + destruct_if as Eq Eq. +Tactic Notation "destruct_if" "in" hyp(H) "as" simple_intropattern(Eq) := + destruct_if in H as Eq Eq. + +Tactic Notation "destruct_if" := + let Eq := fresh "C" in destruct_if as Eq Eq. +Tactic Notation "destruct_if" "in" hyp(H) := + let Eq := fresh "C" in destruct_if in H as Eq Eq. + + +(** ---BROKEN since v8.5beta2. + + [destruct_head_match] performs a case analysis on the argument + of the head pattern matching when the goal has the form + [match ?E with ...] or [match ?E with ... = _] or + [_ = match ?E with ...]. Due to the limits of Ltac, this tactic + will not fail if a match does not occur. Instead, it might + perform a case analysis on an unspecified subterm from the goal. + Warning: experimental. *) + +Ltac find_head_match T := + match T with context [?E] => + match T with + | E => fail 1 + | _ => constr:(E) + end + end. + +Ltac destruct_head_match_core cont := + match goal with + | |- ?T1 = ?T2 => first [ let E := find_head_match T1 in cont E + | let E := find_head_match T2 in cont E ] + | |- ?T1 => let E := find_head_match T1 in cont E + end; + destruct_if_post. + +Tactic Notation "destruct_head_match" "as" simple_intropattern(I) := + destruct_head_match_core ltac:(fun E => destruct E as I). + +Tactic Notation "destruct_head_match" := + destruct_head_match_core ltac:(fun E => destruct E). + + +(**--provided for compatibility with [remember] *) + +(** [cases' E] is similar to [case_eq E] except that it generates the + equality in the context and not in the goal. The syntax [cases E as H] + allows specifying the name [H] of that hypothesis. *) + +Tactic Notation "cases'" constr(E) "as" ident(H) := + let X := fresh "TEMP" in + set (X := E) in *; def_to_eq X H E; + destruct X. + +Tactic Notation "cases'" constr(E) := + let x := fresh "Eq" in cases' E as H. + +(** [cases_if'] is similar to [cases_if] except that it generates + the symmetric equality. *) + +Ltac cases_if_on' E Eq := + match type of E with + | {_}+{_} => destruct E as [Eq|Eq]; try subst_hyp Eq + | _ => let X := fresh in + sets_eq X Eq: E; + destruct X + end; case_if_post. + +Tactic Notation "cases_if'" "as" simple_intropattern(Eq) := + match goal with + | |- context [if ?B then _ else _] => cases_if_on' B Eq + | K: context [if ?B then _ else _] |- _ => cases_if_on' B Eq + end. + +Tactic Notation "cases_if'" := + let Eq := fresh in cases_if' as Eq. + + +(* ********************************************************************** *) +(** * Induction *) + +(** [inductions E] is a shorthand for [dependent induction E]. + [inductions E gen X1 .. XN] is a shorthand for + [dependent induction E generalizing X1 .. XN]. *) + +Require Import Coq.Program.Equality. + +Ltac inductions_post := + unfold eq' in *. + +Tactic Notation "inductions" ident(E) := + dependent induction E; inductions_post. +Tactic Notation "inductions" ident(E) "gen" ident(X1) := + dependent induction E generalizing X1; inductions_post. +Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) := + dependent induction E generalizing X1 X2; inductions_post. +Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) + ident(X3) := + dependent induction E generalizing X1 X2 X3; inductions_post. +Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) + ident(X3) ident(X4) := + dependent induction E generalizing X1 X2 X3 X4; inductions_post. +Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) + ident(X3) ident(X4) ident(X5) := + dependent induction E generalizing X1 X2 X3 X4 X5; inductions_post. +Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) + ident(X3) ident(X4) ident(X5) ident(X6) := + dependent induction E generalizing X1 X2 X3 X4 X5 X6; inductions_post. +Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) + ident(X3) ident(X4) ident(X5) ident(X6) ident(X7) := + dependent induction E generalizing X1 X2 X3 X4 X5 X6 X7; inductions_post. +Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) + ident(X3) ident(X4) ident(X5) ident(X6) ident(X7) ident(X8) := + dependent induction E generalizing X1 X2 X3 X4 X5 X6 X7 X8; inductions_post. + +(** [induction_wf IH: E X] is used to apply the well-founded induction + principle, for a given well-founded relation. It applies to a goal + [PX] where [PX] is a proposition on [X]. First, it sets up the + goal in the form [(fun a => P a) X], using [pattern X], and then + it applies the well-founded induction principle instantiated on [E], + where [E] is a term of type [well_founded R], and [R] is a binary + relation. + Syntaxes [induction_wf: E X] and [induction_wf E X]. *) + +Tactic Notation "induction_wf" ident(IH) ":" constr(E) ident(X) := + pattern X; apply (well_founded_ind E); clear X; intros X IH. +Tactic Notation "induction_wf" ":" constr(E) ident(X) := + let IH := fresh "IH" in induction_wf IH: E X. +Tactic Notation "induction_wf" ":" constr(E) ident(X) := + induction_wf: E X. + +(** Induction on the height of a derivation: the helper tactic + [induct_height] helps proving the equivalence of the auxiliary + judgment that includes a counter for the maximal height + (see LibTacticsDemos for an example) *) + +Require Import Compare_dec Omega. + +Lemma induct_height_max2 : forall n1 n2 : nat, + exists n, n1 < n /\ n2 < n. +Proof using. + intros. destruct (lt_dec n1 n2). + exists (S n2). omega. + exists (S n1). omega. +Qed. + +Ltac induct_height_step x := + match goal with + | H: exists _, _ |- _ => + let n := fresh "n" in let y := fresh "x" in + destruct H as [n ?]; + forwards (y&?&?): induct_height_max2 n x; + induct_height_step y + | _ => exists (S x); eauto + end. + +Ltac induct_height := induct_height_step O. + + +(* ********************************************************************** *) +(** * Coinduction *) + +(** Tactic [cofixs IH] is like [cofix IH] except that the + coinduction hypothesis is tagged in the form [IH: COIND P] + instead of being just [IH: P]. This helps other tactics + clearing the coinduction hypothesis using [clear_coind] *) + +Definition COIND (P:Prop) := P. + +Tactic Notation "cofixs" ident(IH) := + cofix IH; + match type of IH with ?P => change P with (COIND P) in IH end. + +(** Tactic [clear_coind] clears all the coinduction hypotheses, + assuming that they have been tagged *) + +Ltac clear_coind := + repeat match goal with H: COIND _ |- _ => clear H end. + +(** Tactic [abstracts tac] is like [abstract tac] except that + it clears the coinduction hypotheses so that the productivity + check will be happy. For example, one can use [abstracts omega] + to obtain the same behavior as [omega] but with an auxiliary + lemma being generated. *) + +Tactic Notation "abstracts" tactic(tac) := + clear_coind; tac. + + + +(* ********************************************************************** *) +(** * Decidable equality *) + +(** [decides_equality] is the same as [decide equality] excepts that it + is able to unfold definitions at head of the current goal. *) + +Ltac decides_equality_tactic := + first [ decide equality | progress(unfolds); decides_equality_tactic ]. + +Tactic Notation "decides_equality" := + decides_equality_tactic. + + +(* ********************************************************************** *) +(** * Equivalence *) + +(** [iff H] can be used to prove an equivalence [P <-> Q] and name [H] + the hypothesis obtained in each case. The syntaxes [iff] and [iff H1 H2] + are also available to specify zero or two names. The tactic [iff <- H] + swaps the two subgoals, i.e., produces (Q -> P) as first subgoal. *) + +Lemma iff_intro_swap : forall (P Q : Prop), + (Q -> P) -> (P -> Q) -> (P <-> Q). +Proof using. intuition. Qed. + +Tactic Notation "iff" simple_intropattern(H1) simple_intropattern(H2) := + split; [ intros H1 | intros H2 ]. +Tactic Notation "iff" simple_intropattern(H) := + iff H H. +Tactic Notation "iff" := + let H := fresh "H" in iff H. + +Tactic Notation "iff" "<-" simple_intropattern(H1) simple_intropattern(H2) := + apply iff_intro_swap; [ intros H1 | intros H2 ]. +Tactic Notation "iff" "<-" simple_intropattern(H) := + iff <- H H. +Tactic Notation "iff" "<-" := + let H := fresh "H" in iff <- H. + + +(* ********************************************************************** *) +(** * N-ary Conjunctions and Disjunctions *) + +(* ---------------------------------------------------------------------- *) +(** N-ary Conjunctions Splitting in Goals *) + +(** Underlying implementation of [splits]. *) + +Ltac splits_tactic N := + match N with + | O => fail + | S O => idtac + | S ?N' => split; [| splits_tactic N'] + end. + +Ltac unfold_goal_until_conjunction := + match goal with + | |- _ /\ _ => idtac + | _ => progress(unfolds); unfold_goal_until_conjunction + end. + +Ltac get_term_conjunction_arity T := + match T with + | _ /\ _ /\ _ /\ _ /\ _ /\ _ /\ _ /\ _ => constr:(8) + | _ /\ _ /\ _ /\ _ /\ _ /\ _ /\ _ => constr:(7) + | _ /\ _ /\ _ /\ _ /\ _ /\ _ => constr:(6) + | _ /\ _ /\ _ /\ _ /\ _ => constr:(5) + | _ /\ _ /\ _ /\ _ => constr:(4) + | _ /\ _ /\ _ => constr:(3) + | _ /\ _ => constr:(2) + | _ -> ?T' => get_term_conjunction_arity T' + | _ => let P := get_head T in + let T' := eval unfold P in T in + match T' with + | T => fail 1 + | _ => get_term_conjunction_arity T' + end + (* todo: warning this can loop... *) + end. + +Ltac get_goal_conjunction_arity := + match goal with |- ?T => get_term_conjunction_arity T end. + +(** [splits] applies to a goal of the form [(T1 /\ .. /\ TN)] and + destruct it into [N] subgoals [T1] .. [TN]. If the goal is not a + conjunction, then it unfolds the head definition. *) + +Tactic Notation "splits" := + unfold_goal_until_conjunction; + let N := get_goal_conjunction_arity in + splits_tactic N. + +(** [splits N] is similar to [splits], except that it will unfold as many + definitions as necessary to obtain an [N]-ary conjunction. *) + +Tactic Notation "splits" constr(N) := + let N := nat_from_number N in + splits_tactic N. + +(** [splits_all] will recursively split any conjunction, unfolding + definitions when necessary. Warning: this tactic will loop + on goals of the form [well_founded R]. Todo: fix this *) + +Ltac splits_all_base := repeat split. + +Tactic Notation "splits_all" := + splits_all_base. + + +(* ---------------------------------------------------------------------- *) +(** N-ary Conjunctions Deconstruction *) + +(** Underlying implementation of [destructs]. *) + +Ltac destructs_conjunction_tactic N T := + match N with + | 2 => destruct T as [? ?] + | 3 => destruct T as [? [? ?]] + | 4 => destruct T as [? [? [? ?]]] + | 5 => destruct T as [? [? [? [? ?]]]] + | 6 => destruct T as [? [? [? [? [? ?]]]]] + | 7 => destruct T as [? [? [? [? [? [? ?]]]]]] + end. + +(** [destructs T] allows destructing a term [T] which is a N-ary + conjunction. It is equivalent to [destruct T as (H1 .. HN)], + except that it does not require to manually specify N different + names. *) + +Tactic Notation "destructs" constr(T) := + let TT := type of T in + let N := get_term_conjunction_arity TT in + destructs_conjunction_tactic N T. + +(** [destructs N T] is equivalent to [destruct T as (H1 .. HN)], + except that it does not require to manually specify N different + names. Remark that it is not restricted to N-ary conjunctions. *) + +Tactic Notation "destructs" constr(N) constr(T) := + let N := nat_from_number N in + destructs_conjunction_tactic N T. + + +(* ---------------------------------------------------------------------- *) +(** Proving goals which are N-ary disjunctions *) + +(** Underlying implementation of [branch]. *) + +Ltac branch_tactic K N := + match constr:(K,N) with + | (_,0) => fail 1 + | (0,_) => fail 1 + | (1,1) => idtac + | (1,_) => left + | (S ?K', S ?N') => right; branch_tactic K' N' + end. + +Ltac unfold_goal_until_disjunction := + match goal with + | |- _ \/ _ => idtac + | _ => progress(unfolds); unfold_goal_until_disjunction + end. + +Ltac get_term_disjunction_arity T := + match T with + | _ \/ _ \/ _ \/ _ \/ _ \/ _ \/ _ \/ _ => constr:(8) + | _ \/ _ \/ _ \/ _ \/ _ \/ _ \/ _ => constr:(7) + | _ \/ _ \/ _ \/ _ \/ _ \/ _ => constr:(6) + | _ \/ _ \/ _ \/ _ \/ _ => constr:(5) + | _ \/ _ \/ _ \/ _ => constr:(4) + | _ \/ _ \/ _ => constr:(3) + | _ \/ _ => constr:(2) + | _ -> ?T' => get_term_disjunction_arity T' + | _ => let P := get_head T in + let T' := eval unfold P in T in + match T' with + | T => fail 1 + | _ => get_term_disjunction_arity T' + end + end. + +Ltac get_goal_disjunction_arity := + match goal with |- ?T => get_term_disjunction_arity T end. + +(** [branch N] applies to a goal of the form + [P1 \/ ... \/ PK \/ ... \/ PN] and leaves the goal [PK]. + It only able to unfold the head definition (if there is one), + but for more complex unfolding one should use the tactic + [branch K of N]. *) + +Tactic Notation "branch" constr(K) := + let K := nat_from_number K in + unfold_goal_until_disjunction; + let N := get_goal_disjunction_arity in + branch_tactic K N. + +(** [branch K of N] is similar to [branch K] except that the + arity of the disjunction [N] is given manually, and so this + version of the tactic is able to unfold definitions. + In other words, applies to a goal of the form + [P1 \/ ... \/ PK \/ ... \/ PN] and leaves the goal [PK]. *) + +Tactic Notation "branch" constr(K) "of" constr(N) := + let N := nat_from_number N in + let K := nat_from_number K in + branch_tactic K N. + + +(* ---------------------------------------------------------------------- *) +(** N-ary Disjunction Deconstruction *) + +(** Underlying implementation of [branches]. *) + +Ltac destructs_disjunction_tactic N T := + match N with + | 2 => destruct T as [? | ?] + | 3 => destruct T as [? | [? | ?]] + | 4 => destruct T as [? | [? | [? | ?]]] + | 5 => destruct T as [? | [? | [? | [? | ?]]]] + end. + +(** [branches T] allows destructing a term [T] which is a N-ary + disjunction. It is equivalent to [destruct T as [ H1 | .. | HN ] ], + and produces [N] subgoals corresponding to the [N] possible cases. *) + +Tactic Notation "branches" constr(T) := + let TT := type of T in + let N := get_term_disjunction_arity TT in + destructs_disjunction_tactic N T. + +(** [branches N T] is the same as [branches T] except that the arity is + forced to [N]. This version is useful to unfold definitions + on the fly. *) + +Tactic Notation "branches" constr(N) constr(T) := + let N := nat_from_number N in + destructs_disjunction_tactic N T. + + +(* ---------------------------------------------------------------------- *) +(** N-ary Existentials *) + +(* Underlying implementation of [exists]. *) + +Ltac get_term_existential_arity T := + match T with + | exists x1 x2 x3 x4 x5 x6 x7 x8, _ => constr:(8) + | exists x1 x2 x3 x4 x5 x6 x7, _ => constr:(7) + | exists x1 x2 x3 x4 x5 x6, _ => constr:(6) + | exists x1 x2 x3 x4 x5, _ => constr:(5) + | exists x1 x2 x3 x4, _ => constr:(4) + | exists x1 x2 x3, _ => constr:(3) + | exists x1 x2, _ => constr:(2) + | exists x1, _ => constr:(1) + | _ -> ?T' => get_term_existential_arity T' + | _ => let P := get_head T in + let T' := eval unfold P in T in + match T' with + | T => fail 1 + | _ => get_term_existential_arity T' + end + end. + +Ltac get_goal_existential_arity := + match goal with |- ?T => get_term_existential_arity T end. + +(** [exists T1 ... TN] is a shorthand for [exists T1; ...; exists TN]. + It is intended to prove goals of the form [exist X1 .. XN, P]. + If an argument provided is [__] (double underscore), then an + evar is introduced. [exists T1 .. TN ___] is equivalent to + [exists T1 .. TN __ __ __] with as many [__] as possible. *) + +Tactic Notation "exists_original" constr(T1) := + exists T1. +Tactic Notation "exists" constr(T1) := + match T1 with + | ltac_wild => esplit + | ltac_wilds => repeat esplit + | _ => exists T1 + end. +Tactic Notation "exists" constr(T1) constr(T2) := + exists T1; exists T2. +Tactic Notation "exists" constr(T1) constr(T2) constr(T3) := + exists T1; exists T2; exists T3. +Tactic Notation "exists" constr(T1) constr(T2) constr(T3) constr(T4) := + exists T1; exists T2; exists T3; exists T4. +Tactic Notation "exists" constr(T1) constr(T2) constr(T3) constr(T4) + constr(T5) := + exists T1; exists T2; exists T3; exists T4; exists T5. +Tactic Notation "exists" constr(T1) constr(T2) constr(T3) constr(T4) + constr(T5) constr(T6) := + exists T1; exists T2; exists T3; exists T4; exists T5; exists T6. + +(* The tactic [exists___ N] is short for [exists __ ... __] + with [N] double-underscores. The tactic [exists] is equivalent + to calling [exists___ N], where the value of [N] is obtained + by counting the number of existentials syntactically present + at the head of the goal. The behaviour of [exists] differs + from that of [exists ___] is the case where the goal is a + definition which yields an existential only after unfolding. *) + +Tactic Notation "exists___" constr(N) := + let rec aux N := + match N with + | 0 => idtac + | S ?N' => esplit; aux N' + end in + let N := nat_from_number N in aux N. + + (* todo: deprecated *) +Tactic Notation "exists___" := + let N := get_goal_existential_arity in + exists___ N. + + (* todo: does not seem to work *) +Tactic Notation "exists" := + exists___. + + (* todo: [exists_all] is the new syntax for [exists___] *) +Tactic Notation "exists_all" := exists___. + +(* ---------------------------------------------------------------------- *) +(** Existentials and conjunctions in hypotheses *) + +(** [unpack] or [unpack H] destructs conjunctions and existentials in + all or one hypothesis. *) + +Ltac unpack_core := + repeat match goal with + | H: _ /\ _ |- _ => destruct H + | H: exists a, _ |- _ => destruct H + end. + +Ltac unpack_from H := + first [ progress (unpack_core) + | destruct H; unpack_core ]. + +Tactic Notation "unpack" := + unpack_core. +Tactic Notation "unpack" constr(H) := + unpack_from H. + + +(* ********************************************************************** *) +(** * Tactics to prove typeclass instances *) + +(** [typeclass] is an automation tactic specialized for finding + typeclass instances. *) + +Tactic Notation "typeclass" := + let go _ := eauto with typeclass_instances in + solve [ go tt | constructor; go tt ]. + +(** [solve_typeclass] is a simpler version of [typeclass], to use + in hint tactics for resolving instances *) + +Tactic Notation "solve_typeclass" := + solve [ eauto with typeclass_instances ]. + + +(* ********************************************************************** *) +(** * Tactics to invoke automation *) + + +(* ---------------------------------------------------------------------- *) +(** ** Definitions for parsing compatibility *) + +Tactic Notation "f_equal" := + f_equal. +Tactic Notation "constructor" := + constructor. +Tactic Notation "simple" := + simpl. + +Tactic Notation "split" := + split. + +Tactic Notation "right" := + right. +Tactic Notation "left" := + left. + + +(* ---------------------------------------------------------------------- *) +(** ** [hint] to add hints local to a lemma *) + +(** [hint E] adds [E] as an hypothesis so that automation can use it. + Syntax [hint E1,..,EN] is available *) + +Tactic Notation "hint" constr(E) := + let H := fresh "Hint" in lets H: E. +Tactic Notation "hint" constr(E1) "," constr(E2) := + hint E1; hint E2. +Tactic Notation "hint" constr(E1) "," constr(E2) "," constr(E3) := + hint E1; hint E2; hint(E3). +Tactic Notation "hint" constr(E1) "," constr(E2) "," constr(E3) "," constr(E4) := + hint E1; hint E2; hint(E3); hint(E4 ). + + +(* ---------------------------------------------------------------------- *) +(** ** [jauto], a new automation tactics *) + +(** [jauto] is better at [intuition eauto] because it can open existentials + from the context. In the same time, [jauto] can be faster than + [intuition eauto] because it does not destruct disjunctions from the + context. The strategy of [jauto] can be summarized as follows: + - open all the existentials and conjunctions from the context + - call esplit and split on the existentials and conjunctions in the goal + - call eauto. *) + +Tactic Notation "jauto" := + try solve [ jauto_set; eauto ]. + +Tactic Notation "jauto_fast" := + try solve [ auto | eauto | jauto ]. + +(** [iauto] is a shorthand for [intuition eauto] *) + +Tactic Notation "iauto" := try solve [intuition eauto]. + + +(* ---------------------------------------------------------------------- *) +(** ** Definitions of automation tactics *) + +(** The two following tactics defined the default behaviour of + "light automation" and "strong automation". These tactics + may be redefined at any time using the syntax [Ltac .. ::= ..]. *) + +(** [auto_tilde] is the tactic which will be called each time a symbol + [~] is used after a tactic. *) + +Ltac auto_tilde_default := auto. +Ltac auto_tilde := auto_tilde_default. + +(** [auto_star] is the tactic which will be called each time a symbol + [*] is used after a tactic. *) + +(* SPECIAL VERSION FOR SF*) +Ltac auto_star_default := try solve [ jauto ]. +Ltac auto_star := auto_star_default. + + +(** [autos~] is a notation for tactic [auto_tilde]. It may be followed + by lemmas (or proofs terms) which auto will be able to use + for solving the goal. *) +(** [autos] is an alias for [autos~] *) + +Tactic Notation "autos" := + auto_tilde. +Tactic Notation "autos" "~" := + auto_tilde. +Tactic Notation "autos" "~" constr(E1) := + lets: E1; auto_tilde. +Tactic Notation "autos" "~" constr(E1) constr(E2) := + lets: E1; lets: E2; auto_tilde. +Tactic Notation "autos" "~" constr(E1) constr(E2) constr(E3) := + lets: E1; lets: E2; lets: E3; auto_tilde. + +(** [autos*] is a notation for tactic [auto_star]. It may be followed + by lemmas (or proofs terms) which auto will be able to use + for solving the goal. *) + +Tactic Notation "autos" "*" := + auto_star. +Tactic Notation "autos" "*" constr(E1) := + lets: E1; auto_star. +Tactic Notation "autos" "*" constr(E1) constr(E2) := + lets: E1; lets: E2; auto_star. +Tactic Notation "autos" "*" constr(E1) constr(E2) constr(E3) := + lets: E1; lets: E2; lets: E3; auto_star. + +(** [auto_false] is a version of [auto] able to spot some contradictions. + There is an ad-hoc support for goals in [<->]: split is called first. + [auto_false~] and [auto_false*] are also available. *) + +Ltac auto_false_base cont := + try solve [ + intros_all; try match goal with |- _ <-> _ => split end; + solve [ cont tt | intros_all; false; cont tt ] ]. + +Tactic Notation "auto_false" := + auto_false_base ltac:(fun tt => auto). +Tactic Notation "auto_false" "~" := + auto_false_base ltac:(fun tt => auto_tilde). +Tactic Notation "auto_false" "*" := + auto_false_base ltac:(fun tt => auto_star). + +(* NOT NEEDED FOR SF (incompatible with V8.4) +Tactic Notation "dauto" := + dintuition eauto. +*) + + + +(* ---------------------------------------------------------------------- *) +(** ** Parsing for light automation *) + +(** Any tactic followed by the symbol [~] will have [auto_tilde] called + on all of its subgoals. Three exceptions: + - [cuts] and [asserts] only call [auto] on their first subgoal, + - [apply~] relies on [sapply] rather than [apply], + - [tryfalse~] is defined as [tryfalse by auto_tilde]. + + Some builtin tactics are not defined using tactic notations + and thus cannot be extended, e.g., [simpl] and [unfold]. + For these, notation such as [simpl~] will not be available. *) + +Tactic Notation "equates" "~" constr(E) := + equates E; auto_tilde. +Tactic Notation "equates" "~" constr(n1) constr(n2) := + equates n1 n2; auto_tilde. +Tactic Notation "equates" "~" constr(n1) constr(n2) constr(n3) := + equates n1 n2 n3; auto_tilde. +Tactic Notation "equates" "~" constr(n1) constr(n2) constr(n3) constr(n4) := + equates n1 n2 n3 n4; auto_tilde. + +Tactic Notation "applys_eq" "~" constr(H) constr(E) := + applys_eq H E; auto_tilde. +Tactic Notation "applys_eq" "~" constr(H) constr(n1) constr(n2) := + applys_eq H n1 n2; auto_tilde. +Tactic Notation "applys_eq" "~" constr(H) constr(n1) constr(n2) constr(n3) := + applys_eq H n1 n2 n3; auto_tilde. +Tactic Notation "applys_eq" "~" constr(H) constr(n1) constr(n2) constr(n3) constr(n4) := + applys_eq H n1 n2 n3 n4; auto_tilde. + +Tactic Notation "apply" "~" constr(H) := + sapply H; auto_tilde. + +Tactic Notation "destruct" "~" constr(H) := + destruct H; auto_tilde. +Tactic Notation "destruct" "~" constr(H) "as" simple_intropattern(I) := + destruct H as I; auto_tilde. +Tactic Notation "f_equal" "~" := + f_equal; auto_tilde. +Tactic Notation "induction" "~" constr(H) := + induction H; auto_tilde. +Tactic Notation "inversion" "~" constr(H) := + inversion H; auto_tilde. +Tactic Notation "split" "~" := + split; auto_tilde. +Tactic Notation "subst" "~" := + subst; auto_tilde. +Tactic Notation "right" "~" := + right; auto_tilde. +Tactic Notation "left" "~" := + left; auto_tilde. +Tactic Notation "constructor" "~" := + constructor; auto_tilde. +Tactic Notation "constructors" "~" := + constructors; auto_tilde. + +Tactic Notation "false" "~" := + false; auto_tilde. +Tactic Notation "false" "~" constr(E) := + false_then E ltac:(fun _ => auto_tilde). +Tactic Notation "false" "~" constr(E0) constr(E1) := + false~ (>> E0 E1). +Tactic Notation "false" "~" constr(E0) constr(E1) constr(E2) := + false~ (>> E0 E1 E2). +Tactic Notation "false" "~" constr(E0) constr(E1) constr(E2) constr(E3) := + false~ (>> E0 E1 E2 E3). +Tactic Notation "false" "~" constr(E0) constr(E1) constr(E2) constr(E3) constr(E4) := + false~ (>> E0 E1 E2 E3 E4). +Tactic Notation "tryfalse" "~" := + try solve [ false~ ]. + +Tactic Notation "asserts" "~" simple_intropattern(H) ":" constr(E) := + asserts H: E; [ auto_tilde | idtac ]. +Tactic Notation "asserts" "~" ":" constr(E) := + let H := fresh "H" in asserts~ H: E. +Tactic Notation "cuts" "~" simple_intropattern(H) ":" constr(E) := + cuts H: E; [ auto_tilde | idtac ]. +Tactic Notation "cuts" "~" ":" constr(E) := + cuts: E; [ auto_tilde | idtac ]. + +Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E) := + lets I: E; auto_tilde. +Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) := + lets I: E0 A1; auto_tilde. +Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) := + lets I: E0 A1 A2; auto_tilde. +Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + lets I: E0 A1 A2 A3; auto_tilde. +Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + lets I: E0 A1 A2 A3 A4; auto_tilde. +Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + lets I: E0 A1 A2 A3 A4 A5; auto_tilde. + +Tactic Notation "lets" "~" ":" constr(E) := + lets: E; auto_tilde. +Tactic Notation "lets" "~" ":" constr(E0) + constr(A1) := + lets: E0 A1; auto_tilde. +Tactic Notation "lets" "~" ":" constr(E0) + constr(A1) constr(A2) := + lets: E0 A1 A2; auto_tilde. +Tactic Notation "lets" "~" ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + lets: E0 A1 A2 A3; auto_tilde. +Tactic Notation "lets" "~" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + lets: E0 A1 A2 A3 A4; auto_tilde. +Tactic Notation "lets" "~" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + lets: E0 A1 A2 A3 A4 A5; auto_tilde. + +Tactic Notation "forwards" "~" simple_intropattern(I) ":" constr(E) := + forwards I: E; auto_tilde. +Tactic Notation "forwards" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) := + forwards I: E0 A1; auto_tilde. +Tactic Notation "forwards" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) := + forwards I: E0 A1 A2; auto_tilde. +Tactic Notation "forwards" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + forwards I: E0 A1 A2 A3; auto_tilde. +Tactic Notation "forwards" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + forwards I: E0 A1 A2 A3 A4; auto_tilde. +Tactic Notation "forwards" "~" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + forwards I: E0 A1 A2 A3 A4 A5; auto_tilde. + +Tactic Notation "forwards" "~" ":" constr(E) := + forwards: E; auto_tilde. +Tactic Notation "forwards" "~" ":" constr(E0) + constr(A1) := + forwards: E0 A1; auto_tilde. +Tactic Notation "forwards" "~" ":" constr(E0) + constr(A1) constr(A2) := + forwards: E0 A1 A2; auto_tilde. +Tactic Notation "forwards" "~" ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + forwards: E0 A1 A2 A3; auto_tilde. +Tactic Notation "forwards" "~" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + forwards: E0 A1 A2 A3 A4; auto_tilde. +Tactic Notation "forwards" "~" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + forwards: E0 A1 A2 A3 A4 A5; auto_tilde. + +Tactic Notation "applys" "~" constr(H) := + sapply H; auto_tilde. (*todo?*) +Tactic Notation "applys" "~" constr(E0) constr(A1) := + applys E0 A1; auto_tilde. +Tactic Notation "applys" "~" constr(E0) constr(A1) := + applys E0 A1; auto_tilde. +Tactic Notation "applys" "~" constr(E0) constr(A1) constr(A2) := + applys E0 A1 A2; auto_tilde. +Tactic Notation "applys" "~" constr(E0) constr(A1) constr(A2) constr(A3) := + applys E0 A1 A2 A3; auto_tilde. +Tactic Notation "applys" "~" constr(E0) constr(A1) constr(A2) constr(A3) constr(A4) := + applys E0 A1 A2 A3 A4; auto_tilde. +Tactic Notation "applys" "~" constr(E0) constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + applys E0 A1 A2 A3 A4 A5; auto_tilde. + +Tactic Notation "specializes" "~" hyp(H) := + specializes H; auto_tilde. +Tactic Notation "specializes" "~" hyp(H) constr(A1) := + specializes H A1; auto_tilde. +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) := + specializes H A1 A2; auto_tilde. +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) constr(A3) := + specializes H A1 A2 A3; auto_tilde. +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) constr(A3) constr(A4) := + specializes H A1 A2 A3 A4; auto_tilde. +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + specializes H A1 A2 A3 A4 A5; auto_tilde. + +Tactic Notation "fapply" "~" constr(E) := + fapply E; auto_tilde. +Tactic Notation "sapply" "~" constr(E) := + sapply E; auto_tilde. + +Tactic Notation "logic" "~" constr(E) := + logic_base E ltac:(fun _ => auto_tilde). + +Tactic Notation "intros_all" "~" := + intros_all; auto_tilde. + +Tactic Notation "unfolds" "~" := + unfolds; auto_tilde. +Tactic Notation "unfolds" "~" constr(F1) := + unfolds F1; auto_tilde. +Tactic Notation "unfolds" "~" constr(F1) "," constr(F2) := + unfolds F1, F2; auto_tilde. +Tactic Notation "unfolds" "~" constr(F1) "," constr(F2) "," constr(F3) := + unfolds F1, F2, F3; auto_tilde. +Tactic Notation "unfolds" "~" constr(F1) "," constr(F2) "," constr(F3) "," + constr(F4) := + unfolds F1, F2, F3, F4; auto_tilde. + +Tactic Notation "simple" "~" := + simpl; auto_tilde. +Tactic Notation "simple" "~" "in" hyp(H) := + simpl in H; auto_tilde. +Tactic Notation "simpls" "~" := + simpls; auto_tilde. +Tactic Notation "hnfs" "~" := + hnfs; auto_tilde. +Tactic Notation "hnfs" "~" "in" hyp(H) := + hnf in H; auto_tilde. +Tactic Notation "substs" "~" := + substs; auto_tilde. +Tactic Notation "intro_hyp" "~" hyp(H) := + subst_hyp H; auto_tilde. +Tactic Notation "intro_subst" "~" := + intro_subst; auto_tilde. +Tactic Notation "subst_eq" "~" constr(E) := + subst_eq E; auto_tilde. + +Tactic Notation "rewrite" "~" constr(E) := + rewrite E; auto_tilde. +Tactic Notation "rewrite" "~" "<-" constr(E) := + rewrite <- E; auto_tilde. +Tactic Notation "rewrite" "~" constr(E) "in" hyp(H) := + rewrite E in H; auto_tilde. +Tactic Notation "rewrite" "~" "<-" constr(E) "in" hyp(H) := + rewrite <- E in H; auto_tilde. + +Tactic Notation "rewrites" "~" constr(E) := + rewrites E; auto_tilde. +Tactic Notation "rewrites" "~" constr(E) "in" hyp(H) := + rewrites E in H; auto_tilde. +Tactic Notation "rewrites" "~" constr(E) "in" "*" := + rewrites E in *; auto_tilde. +Tactic Notation "rewrites" "~" "<-" constr(E) := + rewrites <- E; auto_tilde. +Tactic Notation "rewrites" "~" "<-" constr(E) "in" hyp(H) := + rewrites <- E in H; auto_tilde. +Tactic Notation "rewrites" "~" "<-" constr(E) "in" "*" := + rewrites <- E in *; auto_tilde. + +Tactic Notation "rewrite_all" "~" constr(E) := + rewrite_all E; auto_tilde. +Tactic Notation "rewrite_all" "~" "<-" constr(E) := + rewrite_all <- E; auto_tilde. +Tactic Notation "rewrite_all" "~" constr(E) "in" ident(H) := + rewrite_all E in H; auto_tilde. +Tactic Notation "rewrite_all" "~" "<-" constr(E) "in" ident(H) := + rewrite_all <- E in H; auto_tilde. +Tactic Notation "rewrite_all" "~" constr(E) "in" "*" := + rewrite_all E in *; auto_tilde. +Tactic Notation "rewrite_all" "~" "<-" constr(E) "in" "*" := + rewrite_all <- E in *; auto_tilde. + +Tactic Notation "asserts_rewrite" "~" constr(E) := + asserts_rewrite E; auto_tilde. +Tactic Notation "asserts_rewrite" "~" "<-" constr(E) := + asserts_rewrite <- E; auto_tilde. +Tactic Notation "asserts_rewrite" "~" constr(E) "in" hyp(H) := + asserts_rewrite E in H; auto_tilde. +Tactic Notation "asserts_rewrite" "~" "<-" constr(E) "in" hyp(H) := + asserts_rewrite <- E in H; auto_tilde. +Tactic Notation "asserts_rewrite" "~" constr(E) "in" "*" := + asserts_rewrite E in *; auto_tilde. +Tactic Notation "asserts_rewrite" "~" "<-" constr(E) "in" "*" := + asserts_rewrite <- E in *; auto_tilde. + +Tactic Notation "cuts_rewrite" "~" constr(E) := + cuts_rewrite E; auto_tilde. +Tactic Notation "cuts_rewrite" "~" "<-" constr(E) := + cuts_rewrite <- E; auto_tilde. +Tactic Notation "cuts_rewrite" "~" constr(E) "in" hyp(H) := + cuts_rewrite E in H; auto_tilde. +Tactic Notation "cuts_rewrite" "~" "<-" constr(E) "in" hyp(H) := + cuts_rewrite <- E in H; auto_tilde. + +Tactic Notation "erewrite" "~" constr(E) := + erewrite E; auto_tilde. + +Tactic Notation "fequal" "~" := + fequal; auto_tilde. +Tactic Notation "fequals" "~" := + fequals; auto_tilde. +Tactic Notation "pi_rewrite" "~" constr(E) := + pi_rewrite E; auto_tilde. +Tactic Notation "pi_rewrite" "~" constr(E) "in" hyp(H) := + pi_rewrite E in H; auto_tilde. + +Tactic Notation "invert" "~" hyp(H) := + invert H; auto_tilde. +Tactic Notation "inverts" "~" hyp(H) := + inverts H; auto_tilde. +Tactic Notation "inverts" "~" hyp(E) "as" := + inverts E as; auto_tilde. +Tactic Notation "injects" "~" hyp(H) := + injects H; auto_tilde. +Tactic Notation "inversions" "~" hyp(H) := + inversions H; auto_tilde. + +Tactic Notation "cases" "~" constr(E) "as" ident(H) := + cases E as H; auto_tilde. +Tactic Notation "cases" "~" constr(E) := + cases E; auto_tilde. +Tactic Notation "case_if" "~" := + case_if; auto_tilde. +Tactic Notation "case_ifs" "~" := + case_ifs; auto_tilde. +Tactic Notation "case_if" "~" "in" hyp(H) := + case_if in H; auto_tilde. +Tactic Notation "cases_if" "~" := + cases_if; auto_tilde. +Tactic Notation "cases_if" "~" "in" hyp(H) := + cases_if in H; auto_tilde. +Tactic Notation "destruct_if" "~" := + destruct_if; auto_tilde. +Tactic Notation "destruct_if" "~" "in" hyp(H) := + destruct_if in H; auto_tilde. +Tactic Notation "destruct_head_match" "~" := + destruct_head_match; auto_tilde. + +Tactic Notation "cases'" "~" constr(E) "as" ident(H) := + cases' E as H; auto_tilde. +Tactic Notation "cases'" "~" constr(E) := + cases' E; auto_tilde. +Tactic Notation "cases_if'" "~" "as" ident(H) := + cases_if' as H; auto_tilde. +Tactic Notation "cases_if'" "~" := + cases_if'; auto_tilde. + +Tactic Notation "decides_equality" "~" := + decides_equality; auto_tilde. + +Tactic Notation "iff" "~" := + iff; auto_tilde. +Tactic Notation "splits" "~" := + splits; auto_tilde. +Tactic Notation "splits" "~" constr(N) := + splits N; auto_tilde. +Tactic Notation "splits_all" "~" := + splits_all; auto_tilde. + +Tactic Notation "destructs" "~" constr(T) := + destructs T; auto_tilde. +Tactic Notation "destructs" "~" constr(N) constr(T) := + destructs N T; auto_tilde. + +Tactic Notation "branch" "~" constr(N) := + branch N; auto_tilde. +Tactic Notation "branch" "~" constr(K) "of" constr(N) := + branch K of N; auto_tilde. + +Tactic Notation "branches" "~" constr(T) := + branches T; auto_tilde. +Tactic Notation "branches" "~" constr(N) constr(T) := + branches N T; auto_tilde. + +Tactic Notation "exists" "~" := + exists; auto_tilde. +Tactic Notation "exists___" "~" := + exists___; auto_tilde. +Tactic Notation "exists" "~" constr(T1) := + exists T1; auto_tilde. +Tactic Notation "exists" "~" constr(T1) constr(T2) := + exists T1 T2; auto_tilde. +Tactic Notation "exists" "~" constr(T1) constr(T2) constr(T3) := + exists T1 T2 T3; auto_tilde. +Tactic Notation "exists" "~" constr(T1) constr(T2) constr(T3) constr(T4) := + exists T1 T2 T3 T4; auto_tilde. +Tactic Notation "exists" "~" constr(T1) constr(T2) constr(T3) constr(T4) + constr(T5) := + exists T1 T2 T3 T4 T5; auto_tilde. +Tactic Notation "exists" "~" constr(T1) constr(T2) constr(T3) constr(T4) + constr(T5) constr(T6) := + exists T1 T2 T3 T4 T5 T6; auto_tilde. + + +(* ---------------------------------------------------------------------- *) +(** ** Parsing for strong automation *) + +(** Any tactic followed by the symbol [*] will have [auto*] called + on all of its subgoals. The exceptions to these rules are the + same as for light automation. + + Exception: use [subs*] instead of [subst*] if you + import the library [Coq.Classes.Equivalence]. *) + +Tactic Notation "equates" "*" constr(E) := + equates E; auto_star. +Tactic Notation "equates" "*" constr(n1) constr(n2) := + equates n1 n2; auto_star. +Tactic Notation "equates" "*" constr(n1) constr(n2) constr(n3) := + equates n1 n2 n3; auto_star. +Tactic Notation "equates" "*" constr(n1) constr(n2) constr(n3) constr(n4) := + equates n1 n2 n3 n4; auto_star. + +Tactic Notation "applys_eq" "*" constr(H) constr(E) := + applys_eq H E; auto_star. +Tactic Notation "applys_eq" "*" constr(H) constr(n1) constr(n2) := + applys_eq H n1 n2; auto_star. +Tactic Notation "applys_eq" "*" constr(H) constr(n1) constr(n2) constr(n3) := + applys_eq H n1 n2 n3; auto_star. +Tactic Notation "applys_eq" "*" constr(H) constr(n1) constr(n2) constr(n3) constr(n4) := + applys_eq H n1 n2 n3 n4; auto_star. + +Tactic Notation "apply" "*" constr(H) := + sapply H; auto_star. + +Tactic Notation "destruct" "*" constr(H) := + destruct H; auto_star. +Tactic Notation "destruct" "*" constr(H) "as" simple_intropattern(I) := + destruct H as I; auto_star. +Tactic Notation "f_equal" "*" := + f_equal; auto_star. +Tactic Notation "induction" "*" constr(H) := + induction H; auto_star. +Tactic Notation "inversion" "*" constr(H) := + inversion H; auto_star. +Tactic Notation "split" "*" := + split; auto_star. +Tactic Notation "subs" "*" := + subst; auto_star. +Tactic Notation "subst" "*" := + subst; auto_star. +Tactic Notation "right" "*" := + right; auto_star. +Tactic Notation "left" "*" := + left; auto_star. +Tactic Notation "constructor" "*" := + constructor; auto_star. +Tactic Notation "constructors" "*" := + constructors; auto_star. + +Tactic Notation "false" "*" := + false; auto_star. +Tactic Notation "false" "*" constr(E) := + false_then E ltac:(fun _ => auto_star). +Tactic Notation "false" "*" constr(E0) constr(E1) := + false* (>> E0 E1). +Tactic Notation "false" "*" constr(E0) constr(E1) constr(E2) := + false* (>> E0 E1 E2). +Tactic Notation "false" "*" constr(E0) constr(E1) constr(E2) constr(E3) := + false* (>> E0 E1 E2 E3). +Tactic Notation "false" "*" constr(E0) constr(E1) constr(E2) constr(E3) constr(E4) := + false* (>> E0 E1 E2 E3 E4). +Tactic Notation "tryfalse" "*" := + try solve [ false* ]. + +Tactic Notation "asserts" "*" simple_intropattern(H) ":" constr(E) := + asserts H: E; [ auto_star | idtac ]. +Tactic Notation "asserts" "*" ":" constr(E) := + let H := fresh "H" in asserts* H: E. +Tactic Notation "cuts" "*" simple_intropattern(H) ":" constr(E) := + cuts H: E; [ auto_star | idtac ]. +Tactic Notation "cuts" "*" ":" constr(E) := + cuts: E; [ auto_star | idtac ]. + +Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E) := + lets I: E; auto_star. +Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) := + lets I: E0 A1; auto_star. +Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) := + lets I: E0 A1 A2; auto_star. +Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + lets I: E0 A1 A2 A3; auto_star. +Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + lets I: E0 A1 A2 A3 A4; auto_star. +Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + lets I: E0 A1 A2 A3 A4 A5; auto_star. + +Tactic Notation "lets" "*" ":" constr(E) := + lets: E; auto_star. +Tactic Notation "lets" "*" ":" constr(E0) + constr(A1) := + lets: E0 A1; auto_star. +Tactic Notation "lets" "*" ":" constr(E0) + constr(A1) constr(A2) := + lets: E0 A1 A2; auto_star. +Tactic Notation "lets" "*" ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + lets: E0 A1 A2 A3; auto_star. +Tactic Notation "lets" "*" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + lets: E0 A1 A2 A3 A4; auto_star. +Tactic Notation "lets" "*" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + lets: E0 A1 A2 A3 A4 A5; auto_star. + +Tactic Notation "forwards" "*" simple_intropattern(I) ":" constr(E) := + forwards I: E; auto_star. +Tactic Notation "forwards" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) := + forwards I: E0 A1; auto_star. +Tactic Notation "forwards" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) := + forwards I: E0 A1 A2; auto_star. +Tactic Notation "forwards" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + forwards I: E0 A1 A2 A3; auto_star. +Tactic Notation "forwards" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + forwards I: E0 A1 A2 A3 A4; auto_star. +Tactic Notation "forwards" "*" simple_intropattern(I) ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + forwards I: E0 A1 A2 A3 A4 A5; auto_star. + +Tactic Notation "forwards" "*" ":" constr(E) := + forwards: E; auto_star. +Tactic Notation "forwards" "*" ":" constr(E0) + constr(A1) := + forwards: E0 A1; auto_star. +Tactic Notation "forwards" "*" ":" constr(E0) + constr(A1) constr(A2) := + forwards: E0 A1 A2; auto_star. +Tactic Notation "forwards" "*" ":" constr(E0) + constr(A1) constr(A2) constr(A3) := + forwards: E0 A1 A2 A3; auto_star. +Tactic Notation "forwards" "*" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) := + forwards: E0 A1 A2 A3 A4; auto_star. +Tactic Notation "forwards" "*" ":" constr(E0) + constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + forwards: E0 A1 A2 A3 A4 A5; auto_star. + +Tactic Notation "applys" "*" constr(H) := + sapply H; auto_star. (*todo?*) +Tactic Notation "applys" "*" constr(E0) constr(A1) := + applys E0 A1; auto_star. +Tactic Notation "applys" "*" constr(E0) constr(A1) := + applys E0 A1; auto_star. +Tactic Notation "applys" "*" constr(E0) constr(A1) constr(A2) := + applys E0 A1 A2; auto_star. +Tactic Notation "applys" "*" constr(E0) constr(A1) constr(A2) constr(A3) := + applys E0 A1 A2 A3; auto_star. +Tactic Notation "applys" "*" constr(E0) constr(A1) constr(A2) constr(A3) constr(A4) := + applys E0 A1 A2 A3 A4; auto_star. +Tactic Notation "applys" "*" constr(E0) constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + applys E0 A1 A2 A3 A4 A5; auto_star. + +Tactic Notation "specializes" "*" hyp(H) := + specializes H; auto_star. +Tactic Notation "specializes" "~" hyp(H) constr(A1) := + specializes H A1; auto_star. +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) := + specializes H A1 A2; auto_star. +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) constr(A3) := + specializes H A1 A2 A3; auto_star. +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) constr(A3) constr(A4) := + specializes H A1 A2 A3 A4; auto_star. +Tactic Notation "specializes" hyp(H) constr(A1) constr(A2) constr(A3) constr(A4) constr(A5) := + specializes H A1 A2 A3 A4 A5; auto_star. + + +Tactic Notation "fapply" "*" constr(E) := + fapply E; auto_star. +Tactic Notation "sapply" "*" constr(E) := + sapply E; auto_star. + +Tactic Notation "logic" constr(E) := + logic_base E ltac:(fun _ => auto_star). + +Tactic Notation "intros_all" "*" := + intros_all; auto_star. + +Tactic Notation "unfolds" "*" := + unfolds; auto_star. +Tactic Notation "unfolds" "*" constr(F1) := + unfolds F1; auto_star. +Tactic Notation "unfolds" "*" constr(F1) "," constr(F2) := + unfolds F1, F2; auto_star. +Tactic Notation "unfolds" "*" constr(F1) "," constr(F2) "," constr(F3) := + unfolds F1, F2, F3; auto_star. +Tactic Notation "unfolds" "*" constr(F1) "," constr(F2) "," constr(F3) "," + constr(F4) := + unfolds F1, F2, F3, F4; auto_star. + +Tactic Notation "simple" "*" := + simpl; auto_star. +Tactic Notation "simple" "*" "in" hyp(H) := + simpl in H; auto_star. +Tactic Notation "simpls" "*" := + simpls; auto_star. +Tactic Notation "hnfs" "*" := + hnfs; auto_star. +Tactic Notation "hnfs" "*" "in" hyp(H) := + hnf in H; auto_star. +Tactic Notation "substs" "*" := + substs; auto_star. +Tactic Notation "intro_hyp" "*" hyp(H) := + subst_hyp H; auto_star. +Tactic Notation "intro_subst" "*" := + intro_subst; auto_star. +Tactic Notation "subst_eq" "*" constr(E) := + subst_eq E; auto_star. + +Tactic Notation "rewrite" "*" constr(E) := + rewrite E; auto_star. +Tactic Notation "rewrite" "*" "<-" constr(E) := + rewrite <- E; auto_star. +Tactic Notation "rewrite" "*" constr(E) "in" hyp(H) := + rewrite E in H; auto_star. +Tactic Notation "rewrite" "*" "<-" constr(E) "in" hyp(H) := + rewrite <- E in H; auto_star. + +Tactic Notation "rewrites" "*" constr(E) := + rewrites E; auto_star. +Tactic Notation "rewrites" "*" constr(E) "in" hyp(H):= + rewrites E in H; auto_star. +Tactic Notation "rewrites" "*" constr(E) "in" "*":= + rewrites E in *; auto_star. +Tactic Notation "rewrites" "*" "<-" constr(E) := + rewrites <- E; auto_star. +Tactic Notation "rewrites" "*" "<-" constr(E) "in" hyp(H):= + rewrites <- E in H; auto_star. +Tactic Notation "rewrites" "*" "<-" constr(E) "in" "*":= + rewrites <- E in *; auto_star. + +Tactic Notation "rewrite_all" "*" constr(E) := + rewrite_all E; auto_star. +Tactic Notation "rewrite_all" "*" "<-" constr(E) := + rewrite_all <- E; auto_star. +Tactic Notation "rewrite_all" "*" constr(E) "in" ident(H) := + rewrite_all E in H; auto_star. +Tactic Notation "rewrite_all" "*" "<-" constr(E) "in" ident(H) := + rewrite_all <- E in H; auto_star. +Tactic Notation "rewrite_all" "*" constr(E) "in" "*" := + rewrite_all E in *; auto_star. +Tactic Notation "rewrite_all" "*" "<-" constr(E) "in" "*" := + rewrite_all <- E in *; auto_star. + +Tactic Notation "asserts_rewrite" "*" constr(E) := + asserts_rewrite E; auto_star. +Tactic Notation "asserts_rewrite" "*" "<-" constr(E) := + asserts_rewrite <- E; auto_star. +Tactic Notation "asserts_rewrite" "*" constr(E) "in" hyp(H) := + asserts_rewrite E; auto_star. +Tactic Notation "asserts_rewrite" "*" "<-" constr(E) "in" hyp(H) := + asserts_rewrite <- E; auto_star. +Tactic Notation "asserts_rewrite" "*" constr(E) "in" "*" := + asserts_rewrite E in *; auto_tilde. +Tactic Notation "asserts_rewrite" "*" "<-" constr(E) "in" "*" := + asserts_rewrite <- E in *; auto_tilde. + +Tactic Notation "cuts_rewrite" "*" constr(E) := + cuts_rewrite E; auto_star. +Tactic Notation "cuts_rewrite" "*" "<-" constr(E) := + cuts_rewrite <- E; auto_star. +Tactic Notation "cuts_rewrite" "*" constr(E) "in" hyp(H) := + cuts_rewrite E in H; auto_star. +Tactic Notation "cuts_rewrite" "*" "<-" constr(E) "in" hyp(H) := + cuts_rewrite <- E in H; auto_star. + +Tactic Notation "erewrite" "*" constr(E) := + erewrite E; auto_star. + +Tactic Notation "fequal" "*" := + fequal; auto_star. +Tactic Notation "fequals" "*" := + fequals; auto_star. +Tactic Notation "pi_rewrite" "*" constr(E) := + pi_rewrite E; auto_star. +Tactic Notation "pi_rewrite" "*" constr(E) "in" hyp(H) := + pi_rewrite E in H; auto_star. + +Tactic Notation "invert" "*" hyp(H) := + invert H; auto_star. +Tactic Notation "inverts" "*" hyp(H) := + inverts H; auto_star. +Tactic Notation "inverts" "*" hyp(E) "as" := + inverts E as; auto_star. +Tactic Notation "injects" "*" hyp(H) := + injects H; auto_star. +Tactic Notation "inversions" "*" hyp(H) := + inversions H; auto_star. + +Tactic Notation "cases" "*" constr(E) "as" ident(H) := + cases E as H; auto_star. +Tactic Notation "cases" "*" constr(E) := + cases E; auto_star. +Tactic Notation "case_if" "*" := + case_if; auto_star. +Tactic Notation "case_ifs" "*" := + case_ifs; auto_star. +Tactic Notation "case_if" "*" "in" hyp(H) := + case_if in H; auto_star. +Tactic Notation "cases_if" "*" := + cases_if; auto_star. +Tactic Notation "cases_if" "*" "in" hyp(H) := + cases_if in H; auto_star. + Tactic Notation "destruct_if" "*" := + destruct_if; auto_star. +Tactic Notation "destruct_if" "*" "in" hyp(H) := + destruct_if in H; auto_star. +Tactic Notation "destruct_head_match" "*" := + destruct_head_match; auto_star. + +Tactic Notation "cases'" "*" constr(E) "as" ident(H) := + cases' E as H; auto_star. +Tactic Notation "cases'" "*" constr(E) := + cases' E; auto_star. +Tactic Notation "cases_if'" "*" "as" ident(H) := + cases_if' as H; auto_star. +Tactic Notation "cases_if'" "*" := + cases_if'; auto_star. + + +Tactic Notation "decides_equality" "*" := + decides_equality; auto_star. + +Tactic Notation "iff" "*" := + iff; auto_star. +Tactic Notation "iff" "*" simple_intropattern(I) := + iff I; auto_star. +Tactic Notation "splits" "*" := + splits; auto_star. +Tactic Notation "splits" "*" constr(N) := + splits N; auto_star. +Tactic Notation "splits_all" "*" := + splits_all; auto_star. + +Tactic Notation "destructs" "*" constr(T) := + destructs T; auto_star. +Tactic Notation "destructs" "*" constr(N) constr(T) := + destructs N T; auto_star. + +Tactic Notation "branch" "*" constr(N) := + branch N; auto_star. +Tactic Notation "branch" "*" constr(K) "of" constr(N) := + branch K of N; auto_star. + +Tactic Notation "branches" "*" constr(T) := + branches T; auto_star. +Tactic Notation "branches" "*" constr(N) constr(T) := + branches N T; auto_star. + +Tactic Notation "exists" "*" := + exists; auto_star. +Tactic Notation "exists___" "*" := + exists___; auto_star. +Tactic Notation "exists" "*" constr(T1) := + exists T1; auto_star. +Tactic Notation "exists" "*" constr(T1) constr(T2) := + exists T1 T2; auto_star. +Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) := + exists T1 T2 T3; auto_star. +Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) constr(T4) := + exists T1 T2 T3 T4; auto_star. +Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) constr(T4) + constr(T5) := + exists T1 T2 T3 T4 T5; auto_star. +Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) constr(T4) + constr(T5) constr(T6) := + exists T1 T2 T3 T4 T5 T6; auto_star. + + + +(* ********************************************************************** *) +(** * Tactics to sort out the proof context *) + +(* ---------------------------------------------------------------------- *) +(** ** Hiding hypotheses *) + +(* Implementation *) + +Definition ltac_something (P:Type) (e:P) := e. + +Notation "'Something'" := + (@ltac_something _ _). + +Lemma ltac_something_eq : forall (e:Type), + e = (@ltac_something _ e). +Proof using. auto. Qed. + +Lemma ltac_something_hide : forall (e:Type), + e -> (@ltac_something _ e). +Proof using. auto. Qed. + +Lemma ltac_something_show : forall (e:Type), + (@ltac_something _ e) -> e. +Proof using. auto. Qed. + +(** [hide_def x] and [show_def x] can be used to hide/show + the body of the definition [x]. *) + +Tactic Notation "hide_def" hyp(x) := + let x' := constr:(x) in + let T := eval unfold x in x' in + change T with (@ltac_something _ T) in x. + +Tactic Notation "show_def" hyp(x) := + let x' := constr:(x) in + let U := eval unfold x in x' in + match U with @ltac_something _ ?T => + change U with T in x end. + +(** [show_def] unfolds [Something] in the goal *) + +Tactic Notation "show_def" := + unfold ltac_something. +Tactic Notation "show_def" "in" hyp(H) := + unfold ltac_something in H. +Tactic Notation "show_def" "in" "*" := + unfold ltac_something in *. + +(** [hide_defs] and [show_defs] applies to all definitions *) + +Tactic Notation "hide_defs" := + repeat match goal with H := ?T |- _ => + match T with + | @ltac_something _ _ => fail 1 + | _ => change T with (@ltac_something _ T) in H + end + end. + +Tactic Notation "show_defs" := + repeat match goal with H := (@ltac_something _ ?T) |- _ => + change (@ltac_something _ T) with T in H end. + + +(** [hide_hyp H] replaces the type of [H] with the notation [Something] + and [show_hyp H] reveals the type of the hypothesis. Note that the + hidden type of [H] remains convertible the real type of [H]. *) + +Tactic Notation "show_hyp" hyp(H) := + apply ltac_something_show in H. + +Tactic Notation "hide_hyp" hyp(H) := + apply ltac_something_hide in H. + +(** [hide_hyps] and [show_hyps] can be used to hide/show all hypotheses + of type [Prop]. *) + +Tactic Notation "show_hyps" := + repeat match goal with + H: @ltac_something _ _ |- _ => show_hyp H end. + +Tactic Notation "hide_hyps" := + repeat match goal with H: ?T |- _ => + match type of T with + | Prop => + match T with + | @ltac_something _ _ => fail 2 + | _ => hide_hyp H + end + | _ => fail 1 + end + end. + +(** [hide H] and [show H] automatically select between + [hide_hyp] or [hide_def], and [show_hyp] or [show_def]. + Similarly [hide_all] and [show_all] apply to all. *) + +Tactic Notation "hide" hyp(H) := + first [hide_def H | hide_hyp H]. + +Tactic Notation "show" hyp(H) := + first [show_def H | show_hyp H]. + +Tactic Notation "hide_all" := + hide_hyps; hide_defs. + +Tactic Notation "show_all" := + unfold ltac_something in *. + +(** [hide_term E] can be used to hide a term from the goal. + [show_term] or [show_term E] can be used to reveal it. + [hide_term E in H] can be used to specify an hypothesis. *) + +Tactic Notation "hide_term" constr(E) := + change E with (@ltac_something _ E). +Tactic Notation "show_term" constr(E) := + change (@ltac_something _ E) with E. +Tactic Notation "show_term" := + unfold ltac_something. + +Tactic Notation "hide_term" constr(E) "in" hyp(H) := + change E with (@ltac_something _ E) in H. +Tactic Notation "show_term" constr(E) "in" hyp(H) := + change (@ltac_something _ E) with E in H. +Tactic Notation "show_term" "in" hyp(H) := + unfold ltac_something in H. + +(** [show_unfold R] unfolds the definition of [R] and + reveals the hidden definition of R. --todo:test, + and implement using unfold simply *) + (* todo: change "unfolds" *) + +Tactic Notation "show_unfold" constr(R1) := + unfold R1; show_def. +Tactic Notation "show_unfold" constr(R1) "," constr(R2) := + unfold R1, R2; show_def. + +(* ---------------------------------------------------------------------- *) +(** ** Sorting hypotheses *) + +(** [sort] sorts out hypotheses from the context by moving all the + propositions (hypotheses of type Prop) to the bottom of the context. *) + +Ltac sort_tactic := + try match goal with H: ?T |- _ => + match type of T with Prop => + generalizes H; (try sort_tactic); intro + end end. + +Tactic Notation "sort" := + sort_tactic. + + +(* ---------------------------------------------------------------------- *) +(** ** Clearing hypotheses *) + +(** [clears X1 ... XN] is a variation on [clear] which clears + the variables [X1]..[XN] as well as all the hypotheses which + depend on them. Contrary to [clear], it never fails. *) + +Tactic Notation "clears" ident(X1) := + let rec doit _ := + match goal with + | H:context[X1] |- _ => clear H; try (doit tt) + | _ => clear X1 + end in doit tt. +Tactic Notation "clears" ident(X1) ident(X2) := + clears X1; clears X2. +Tactic Notation "clears" ident(X1) ident(X2) ident(X3) := + clears X1; clears X2; clears X3. +Tactic Notation "clears" ident(X1) ident(X2) ident(X3) ident(X4) := + clears X1; clears X2; clears X3; clears X4. +Tactic Notation "clears" ident(X1) ident(X2) ident(X3) ident(X4) + ident(X5) := + clears X1; clears X2; clears X3; clears X4; clears X5. +Tactic Notation "clears" ident(X1) ident(X2) ident(X3) ident(X4) + ident(X5) ident(X6) := + clears X1; clears X2; clears X3; clears X4; clears X5; clears X6. + +(** [clears] (without any argument) clears all the unused variables + from the context. In other words, it removes any variable + which is not a proposition (i.e., not of type Prop) and which + does not appear in another hypothesis nor in the goal. *) + (* todo: rename to clears_var ? *) + +Ltac clears_tactic := + match goal with H: ?T |- _ => + match type of T with + | Prop => generalizes H; (try clears_tactic); intro + | ?TT => clear H; (try clears_tactic) + | ?TT => generalizes H; (try clears_tactic); intro + end end. + +Tactic Notation "clears" := + clears_tactic. + +(** [clears_all] clears all the hypotheses from the context + that can be cleared. It leaves only the hypotheses that + are mentioned in the goal. *) + +Ltac clears_or_generalizes_all_core := + repeat match goal with H: _ |- _ => + first [ clear H | generalizes H] end. + +Tactic Notation "clears_all" := + generalize ltac_mark; + clears_or_generalizes_all_core; + intro_until_mark. + +(** [clears_but H1 H2 .. HN] clears all hypotheses except the + one that are mentioned and those that cannot be cleared. *) + +Ltac clears_but_core cont := + generalize ltac_mark; + cont tt; + clears_or_generalizes_all_core; + intro_until_mark. + +Tactic Notation "clears_but" := + clears_but_core ltac:(fun _ => idtac). +Tactic Notation "clears_but" ident(H1) := + clears_but_core ltac:(fun _ => gen H1). +Tactic Notation "clears_but" ident(H1) ident(H2) := + clears_but_core ltac:(fun _ => gen H1 H2). +Tactic Notation "clears_but" ident(H1) ident(H2) ident(H3) := + clears_but_core ltac:(fun _ => gen H1 H2 H3). +Tactic Notation "clears_but" ident(H1) ident(H2) ident(H3) ident(H4) := + clears_but_core ltac:(fun _ => gen H1 H2 H3 H4). +Tactic Notation "clears_but" ident(H1) ident(H2) ident(H3) ident(H4) ident(H5) := + clears_but_core ltac:(fun _ => gen H1 H2 H3 H4 H5). + +Lemma demo_clears_all_and_clears_but : + forall x y:nat, y < 2 -> x = x -> x >= 2 -> x < 3 -> True. +Proof using. + introv M1 M2 M3. dup 6. + (* [clears_all] clears all hypotheses. *) + clears_all. auto. + (* [clears_but H] clears all but [H] *) + clears_but M3. auto. + clears_but y. auto. + clears_but x. auto. + clears_but M2 M3. auto. + clears_but x y. auto. +Qed. + +(** [clears_last] clears the last hypothesis in the context. + [clears_last N] clears the last [N] hypotheses in the context. *) + +Tactic Notation "clears_last" := + match goal with H: ?T |- _ => clear H end. + +Ltac clears_last_base N := + match nat_from_number N with + | 0 => idtac + | S ?p => clears_last; clears_last_base p + end. + +Tactic Notation "clears_last" constr(N) := + clears_last_base N. + + +(* ********************************************************************** *) +(** * Tactics for development purposes *) + +(* ---------------------------------------------------------------------- *) +(** ** Skipping subgoals *) + +(** DEPRECATED: the new "admit" tactics now works fine. + + The [skip] tactic can be used at any time to admit the current + goal. Using [skip] is much more efficient than using the [Focus] + top-level command to reach a particular subgoal. + + There are two possible implementations of [skip]. The first one + relies on the use of an existential variable. The second one + relies on an axiom of type [False]. Remark that the builtin tactic + [admit] is not applicable if the current goal contains uninstantiated + variables. + + The advantage of the first technique is that a proof using [skip] + must end with [Admitted], since [Qed] will be rejected with the message + "[uninstantiated existential variables]". It is thereafter clear + that the development is incomplete. + + The advantage of the second technique is exactly the converse: one + may conclude the proof using [Qed], and thus one saves the pain from + renaming [Qed] into [Admitted] and vice-versa all the time. + Note however, that it is still necessary to instantiate all the existential + variables introduced by other tactics in order for [Qed] to be accepted. + + The two implementation are provided, so that you can select the one that + suits you best. By default [skip'] uses the first implementation, and + [skip] uses the second implementation. +*) + +Ltac skip_with_existential := + match goal with |- ?G => + let H := fresh in evar(H:G); eexact H end. + +(* TO BE DEPRECATED: *) +Variable skip_axiom : False. + (* To obtain a safe development, change to [skip_axiom : True] *) +Ltac skip_with_axiom := + elimtype False; apply skip_axiom. + +Tactic Notation "skip" := + skip_with_axiom. +Tactic Notation "skip'" := + skip_with_existential. + +(* SF DOES NOT NEED THIS +(* For backward compatibility *) +Tactic Notation "admit" := + skip. +*) + +(** [demo] is like [admit] but it documents the fact that admit is intended *) +Tactic Notation "demo" := + skip. + +(** [skip H: T] adds an assumption named [H] of type [T] to the + current context, blindly assuming that it is true. + [skip: T] and [skip H_asserts: T] and [skip_asserts: T] + are other possible syntax. + Note that H may be an intro pattern. + The syntax [skip H1 .. HN: T] can be used when [T] is a + conjunction of [N] items. *) + +Tactic Notation "skip" simple_intropattern(I) ":" constr(T) := + asserts I: T; [ skip | ]. +Tactic Notation "skip" ":" constr(T) := + let H := fresh in skip H: T. +Tactic Notation "skip" "~" ":" constr(T) := + skip: T; auto_tilde. +Tactic Notation "skip" "*" ":" constr(T) := + skip: T; auto_star. + +Tactic Notation "skip" simple_intropattern(I1) + simple_intropattern(I2) ":" constr(T) := + skip [I1 I2]: T. +Tactic Notation "skip" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) ":" constr(T) := + skip [I1 [I2 I3]]: T. +Tactic Notation "skip" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) + simple_intropattern(I4) ":" constr(T) := + skip [I1 [I2 [I3 I4]]]: T. +Tactic Notation "skip" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) + simple_intropattern(I4) simple_intropattern(I5) ":" constr(T) := + skip [I1 [I2 [I3 [I4 I5]]]]: T. +Tactic Notation "skip" simple_intropattern(I1) + simple_intropattern(I2) simple_intropattern(I3) + simple_intropattern(I4) simple_intropattern(I5) + simple_intropattern(I6) ":" constr(T) := + skip [I1 [I2 [I3 [I4 [I5 I6]]]]]: T. + +Tactic Notation "skip_asserts" simple_intropattern(I) ":" constr(T) := + skip I: T. +Tactic Notation "skip_asserts" ":" constr(T) := + skip: T. + +(** [skip_cuts T] simply replaces the current goal with [T]. *) + +Tactic Notation "skip_cuts" constr(T) := + cuts: T; [ skip | ]. + +(** [skip_goal H] applies to any goal. It simply assumes + the current goal to be true. The assumption is named "H". + It is useful to set up proof by induction or coinduction. + Syntax [skip_goal] is also accepted.*) + +Tactic Notation "skip_goal" ident(H) := + match goal with |- ?G => skip H: G end. + +Tactic Notation "skip_goal" := + let IH := fresh "IH" in skip_goal IH. + +(** [skip_rewrite T] can be applied when [T] is an equality. + It blindly assumes this equality to be true, and rewrite it in + the goal. *) + +Tactic Notation "skip_rewrite" constr(T) := + let M := fresh in skip_asserts M: T; rewrite M; clear M. + +(** [skip_rewrite T in H] is similar as [rewrite_skip], except that + it rewrites in hypothesis [H]. *) + +Tactic Notation "skip_rewrite" constr(T) "in" hyp(H) := + let M := fresh in skip_asserts M: T; rewrite M in H; clear M. + +(** [skip_rewrites_all T] is similar as [rewrite_skip], except that + it rewrites everywhere (goal and all hypotheses). *) + +Tactic Notation "skip_rewrite_all" constr(T) := + let M := fresh in skip_asserts M: T; rewrite_all M; clear M. + +(** [skip_induction E] applies to any goal. It simply assumes + the current goal to be true (the assumption is named "IH" by + default), and call [destruct E] instead of [induction E]. + It is useful to try and set up a proof by induction + first, and fix the applications of the induction hypotheses + during a second pass on the Proof using. *) +(* TODO: deprecated *) + +Tactic Notation "skip_induction" constr(E) := + let IH := fresh "IH" in skip_goal IH; destruct E. + +Tactic Notation "skip_induction" constr(E) "as" simple_intropattern(I) := + let IH := fresh "IH" in skip_goal IH; destruct E as I. + + +(* ********************************************************************** *) +(** * Compatibility with standard library *) + +(** The module [Program] contains definitions that conflict with the + current module. If you import [Program], either directly or indirectly + (e.g., through [Setoid] or [ZArith]), you will need to import the + compability definitions through the top-level command: + [Import LibTacticsCompatibility]. *) + +Module LibTacticsCompatibility. + Tactic Notation "apply" "*" constr(H) := + sapply H; auto_star. + Tactic Notation "subst" "*" := + subst; auto_star. +End LibTacticsCompatibility. + +Open Scope nat_scope. + + + + +(* ********************************************************************** *) +(** * Additional notations for Coq *) + +(* ---------------------------------------------------------------------- *) +(** ** N-ary Existentials --TODO: DEPRECATED, Coq now supports it. *) + +(** [exists T1 ... TN, P] is a shorthand for + [exists T1, ..., exists TN, P]. Note that + [Coq.Program.Syntax] already defines exists + for arity up to 4. *) + +(* SF DOES NOT NEED +Notation "'exists' x1 ',' P" := + (exists x1, P) + (at level 200, x1 ident, + right associativity) : type_scope. +Notation "'exists' x1 x2 ',' P" := + (exists x1, exists x2, P) + (at level 200, x1 ident, x2 ident, + right associativity) : type_scope. +Notation "'exists' x1 x2 x3 ',' P" := + (exists x1, exists x2, exists x3, P) + (at level 200, x1 ident, x2 ident, x3 ident, + right associativity) : type_scope. +Notation "'exists' x1 x2 x3 x4 ',' P" := + (exists x1, exists x2, exists x3, exists x4, P) + (at level 200, x1 ident, x2 ident, x3 ident, x4 ident, + right associativity) : type_scope. +Notation "'exists' x1 x2 x3 x4 x5 ',' P" := + (exists x1, exists x2, exists x3, exists x4, exists x5, P) + (at level 200, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, + right associativity) : type_scope. +Notation "'exists' x1 x2 x3 x4 x5 x6 ',' P" := + (exists x1, exists x2, exists x3, exists x4, exists x5, exists x6, P) + (at level 200, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, + x6 ident, + right associativity) : type_scope. +Notation "'exists' x1 x2 x3 x4 x5 x6 x7 ',' P" := + (exists x1, exists x2, exists x3, exists x4, exists x5, exists x6, + exists x7, P) + (at level 200, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, + x6 ident, x7 ident, + right associativity) : type_scope. +Notation "'exists' x1 x2 x3 x4 x5 x6 x7 x8 ',' P" := + (exists x1, exists x2, exists x3, exists x4, exists x5, exists x6, + exists x7, exists x8, P) + (at level 200, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, + x6 ident, x7 ident, x8 ident, + right associativity) : type_scope. +Notation "'exists' x1 x2 x3 x4 x5 x6 x7 x8 x9 ',' P" := + (exists x1, exists x2, exists x3, exists x4, exists x5, exists x6, + exists x7, exists x8, exists x9, P) + (at level 200, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, + x6 ident, x7 ident, x8 ident, x9 ident, + right associativity) : type_scope. +Notation "'exists' x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ',' P" := + (exists x1, exists x2, exists x3, exists x4, exists x5, exists x6, + exists x7, exists x8, exists x9, exists x10, P) + (at level 200, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, + x6 ident, x7 ident, x8 ident, x9 ident, x10 ident, + right associativity) : type_scope. + +*) + +(* ---------------------------------------------------------------------- *) +(** ** ['let] bindings (EXPERIMENTAL). *) + +(** The syntax ['let x := v in e] has the same meaning as [let x := v in e] + except that the binding is implemented using a beta-redex that is not + reduced automatically by [simpl]. The ['let] construct therefore makes + it possible to simplify or push to the context let-bindings one by one. *) + +(** Definition of ['let] *) + +Definition let_binding (A B:Type) (v:A) (K:A->B) := K v. + +Notation "''let' x ':=' v 'in' e" := (let_binding v (fun x => e)) + (at level 69, x ident, right associativity, + format "'[v' '[' ''let' x ':=' v 'in' ']' '/' '[' e ']' ']'") + : let_scope. + +Notation "''let' x ':' A ':=' v 'in' e" := (let_binding (v:A) (fun x:A => e)) + (at level 69, x ident, right associativity, + format "'[v' '[' ''let' x ':' A ':=' v 'in' ']' '/' '[' e ']' ']'") + : let_scope. + +Global Open Scope let_scope. + +Lemma let_binding_unfold : forall (A B:Type) (v:A) (K:A->B), + let_binding v K = K v. +Proof using. reflexivity. Qed. + +Ltac let_get_fresh_binding_name K := + match K with (fun x => _) => let y := fresh x in y end. + +(** [let_simpl] finds the first occurence of a ['let] binding and + substitutes it. *) + +Tactic Notation "let_simpl" "in" hyp(H) := + match type of H with context [ let_binding ?v ?K ] => + changes (let_binding v K) with (K v) in H + end. + +Tactic Notation "let_simpl" := + match goal with + | |- context [ let_binding ?v ?K ] => + changes (let_binding v K) with (K v) + | H: context [ let_binding ?v ?K ] |- _ => + let_simpl in H + end. + +Tactic Notation "let_simpl" constr(v) "in" hyp(H) := + repeat match type of H with context [ let_binding v ?K ] => + changes (let_binding v K) with (K v) in H + end. + +Tactic Notation "let_simpl" constr(v) := + repeat match goal with + | |- context [ let_binding v ?K ] => + changes (let_binding v K) with (K v) + | H: context [ let_binding v ?K ] |- _ => + let_simpl v in H + end. + +(** [let_name] finds the first occurence of a ['let] binding and + moves this binding to the proof context. *) + +Tactic Notation "let_name" "in" hyp(H) := + match type of H with context [ let_binding ?v ?K ] => + let x := let_get_fresh_binding_name K in + set_eq x: v in H; + let_simpl in H + end. + +Tactic Notation "let_name" "in" hyp(H) "as" ident(x) := + match type of H with context [ let_binding ?v ?K ] => + set_eq x: v in H; + let_simpl in H + end. + +Tactic Notation "let_name" := + match goal with + | |- context [ let_binding ?v ?K ] => + let x := let_get_fresh_binding_name K in + set_eq x: v; + let_simpl + | H: context [ let_binding ?v ?K ] |- _ => + let_name in H + end. + +Tactic Notation "let_name" "as" ident(x) := + match goal with + | |- context [ let_binding ?v ?K ] => + set_eq x: v; + let_simpl + | H: context [ let_binding ?v ?K ] |- _ => + let_name in H as x + end. + +(** [let_name_all] finds the first occurence of a ['let] binding, + moves this binding to the proof context, and further simplify + all the other ['let] bindings that are binding the same value. + (See LibFixDemos for a practical motivation.) *) + +Tactic Notation "let_name_all" "in" hyp(H) := + match type of H with context [ let_binding ?v ?K ] => + let x := let_get_fresh_binding_name K in + set_eq x: v in H; + let_simpl x in H + end. + +Tactic Notation "let_name_all" "in" hyp(H) "as" ident(x) := + match type of H with context [ let_binding ?v ?K ] => + set_eq x: v in H; + let_simpl x in H + end. + +Tactic Notation "let_name_all" := + match goal with + | |- context [ let_binding ?v ?K ] => + let x := let_get_fresh_binding_name K in + set_eq x: v; + let_simpl x + | H: context [ let_binding ?v ?K ] |- _ => + let_name_all in H + end. + +Tactic Notation "let_name_all" "as" ident(x) := + match goal with + | |- context [ let_binding ?v ?K ] => + set_eq x: v; + let_simpl x + | H: context [ let_binding ?v ?K ] |- _ => + let_name_all in H as x + end. + + +(* ---------------------------------------------------------------------- *) +(* Bugfix for [f_equal] and [fequals]; only supports up to arity 5 *) + +Section FuncEq. +Variables (A1 A2 A3 A4 A5 B : Type). + +Lemma func_eq_1 : forall (f:A1->B) x1 y1, + x1 = y1 -> + f x1 = f y1. +Proof. intros. subst~. Qed. + +Lemma func_eq_2 : forall (f:A1->A2->B) x1 y1 x2 y2, + x1 = y1 -> x2 = y2 -> + f x1 x2 = f y1 y2. +Proof. intros. subst~. Qed. + +Lemma func_eq_3 : forall (f:A1->A2->A3->B) x1 y1 x2 y2 x3 y3, + x1 = y1 -> x2 = y2 -> x3 = y3 -> + f x1 x2 x3 = f y1 y2 y3. +Proof. intros. subst~. Qed. + +Lemma func_eq_4 : forall (f:A1->A2->A3->A4->B) x1 y1 x2 y2 x3 y3 x4 y4, + x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> + f x1 x2 x3 x4 = f y1 y2 y3 y4. +Proof. intros. subst~. Qed. + +Lemma func_eq_5 : forall (f:A1->A2->A3->A4->A5->B) x1 y1 x2 y2 x3 y3 x4 y4 x5 y5, + x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> x5 = y5 -> + f x1 x2 x3 x4 x5 = f y1 y2 y3 y4 y5. +Proof. intros. subst~. Qed. + +End FuncEq. + +Ltac f_equal_fixed := + try ( + first + [ apply func_eq_1 + | apply func_eq_2 + | apply func_eq_3 + | apply func_eq_4 + | apply func_eq_5 ]; + try reflexivity). + + +Ltac fequal_base ::= + let go := f_equal_fixed; [ fequal_base | ] in + match goal with + | |- (_,_,_) = (_,_,_) => go + | |- (_,_,_,_) = (_,_,_,_) => go + | |- (_,_,_,_,_) = (_,_,_,_,_) => go + | |- (_,_,_,_,_,_) = (_,_,_,_,_,_) => go + | |- _ => f_equal_fixed + end. + + +(* ---------------------------------------------------------------------- *) +(* Bugfix for [autorewrite in *], which is currently inefficient *) + +(** Generalize all propositions into the goal *) + +Ltac generalize_all_prop := + repeat match goal with H: ?T |- _ => + match type of T with Prop => + generalizes H + end end. + +(** Work around for inefficiency bug of [autorewrite in *]. + Usage, e.g.: + [Tactic Notation "rew_list" "in" "*" := + autorewrite_in_star_patch + ltac:(fun tt => autorewrite with rew_list)]. *) + +Ltac autorewrite_in_star_patch cont := + generalize ltac_mark; + generalize_all_prop; + cont tt; + intro_until_mark. + + + diff --git a/Libs.v b/Libs.v new file mode 100755 index 0000000..fbf6b2f --- /dev/null +++ b/Libs.v @@ -0,0 +1,80 @@ +Require Export Coq.Bool.Bool. +Require Export Coq.Arith.Arith. +Require Export Coq.Arith.EqNat. +Require Export Coq.omega.Omega. +Require Export Coq.Lists.List. +Require Export Coq.ZArith.ZArith. +Require Export Coq.Numbers.Natural.Peano.NPeano. +Require Export Coq.Setoids.Setoid. +Require Export Coq.Program.Equality. (**r Necessary for 'dependent induction'. *) + +Require Export LibTactics. + + +Ltac autoinjection := + repeat match goal with + | h: ?f _ = ?f _ |- _ => injection h; intros; clear h; subst + | h: ?f _ _ = ?f _ _ |- _ => injection h; intros; clear h; subst + | h: ?f _ _ _ = ?f _ _ _ |- _ => injection h; intros; clear h; subst + | h: ?f _ _ _ _ = ?f _ _ _ _ |- _ => injection h; intros; clear h; subst + | h: ?f _ _ _ _ _ = ?f _ _ _ _ _ |- _ => injection h; intros; clear h; subst + end. + +Ltac go := + simpl in *; + repeat match goal with + | h: ?x = _ |- context[match ?x with _ => _ end] => rewrite h + end; + autoinjection; + try (congruence); + try omega; + subst; + eauto 4 with zarith datatypes; + try (econstructor ; (solve[go])). + +Tactic Notation "go" := try (go; fail). + +Ltac go_with b := + simpl in *; + repeat match goal with + | h: ?x = _ |- context[match ?x with _ => _ end] => rewrite h + end; + autoinjection; + try (congruence); + try omega; + subst; + eauto 4 with zarith datatypes b; + try (econstructor ; (solve[go])). + +Ltac inv H := inversion H; try subst; clear H. + +Tactic Notation "flatten" ident(H) := + repeat match goal with + | H: context[match ?x with | left _ => _ | right _ => _ end] |- _ => destruct x + | H: context[match ?x with | _ => _ end] |- _ => let E := fresh "Eq" in destruct x eqn:E + end; autoinjection; try congruence. + +Tactic Notation "flatten" := + repeat match goal with + | |- context[match ?x with | left _ => _ | right _ => _ end] => destruct x + | |- context[match ?x with | _ => _ end] => let E := fresh "Eq" in destruct x eqn:E + end; autoinjection; try congruence. + +(*Tactic Notation "induction" ident(x) := dependent induction x.*) + +Definition admit {T: Type} : T. Admitted. + +Tactic Notation "solve_by_inversion_step" tactic(t) := + match goal with + | H : _ |- _ => solve [ inversion H; subst; t ] + end + || fail "because the goal is not solvable by inversion.". + +Tactic Notation "solve" "by" "inversion" "1" := + solve_by_inversion_step idtac. +Tactic Notation "solve" "by" "inversion" "2" := + solve_by_inversion_step (solve by inversion 1). +Tactic Notation "solve" "by" "inversion" "3" := + solve_by_inversion_step (solve by inversion 2). +Tactic Notation "solve" "by" "inversion" := + solve by inversion 1. diff --git a/Mealy.v b/Mealy.v new file mode 100644 index 0000000..52b325c --- /dev/null +++ b/Mealy.v @@ -0,0 +1,99 @@ +Require Import base. +Require Import Monoids. + +Class Mealy (state action out : Type) := { + initial : state; + step : state -> action -> state; + output : state -> action -> out +}. + +(** ** Auxiliary functions + +We define a [run] of a machine [M], which is an extension of +the [step] function to lists of actions. We use a shortcut +[do_actions] for running the machine from the [initial] state. *) + + +Fixpoint run `{Mealy state action out} (s : state) (ls : list action) : state := + match ls with + | nil => s + | a::tl => run (step s a) tl + end. + +Definition do_actions `{Mealy state action out} : list action -> state := run initial. + +(** The [test] function runs the required list of actions and examines the output of the resulting state on a specified action. *) +Definition test `{Mealy state action out} (ls : list action) : action -> out := output (do_actions ls). + +Global Instance MealyMRet `{Monoid out op e} : MRet (λ A, (A * out)%type) := + fun A x => (x, e). +Global Instance MealyMBind `{Monoid out op e} : MBind (λ A, (A * out)%type) := + fun A B (f : A → B * out) (x : A * out) => + match x with + (x₁,x₂) => match f x₁ with + (y₁,y₂) => (y₁, op x₂ y₂) + end + end. +Global Instance MealyMonad `{Monoid out op e} `{Mealy state action out} : + Monad (λ A, (A * out)%type). +Proof. split; intros; +unfold mret, mbind; unfold MealyMRet, MealyMBind. +destruct m. rewrite right_id; auto. +apply H. (* TODO: why is this not being picked up automatically? *) + +destruct (f x). rewrite left_id; auto. apply H. + +destruct m. destruct (f a). destruct (g b). +rewrite associative. reflexivity. apply H. +Qed. +About run. + +Class MSync (state action out : Type) + := { + msync_mealy : Mealy state action out; + delayed : action -> (state -> Prop); + delayed_dec :> forall a s, Decision (delayed a s) +}. + +Global Instance MSync_as_Mealy `{MS: MSync state action out} + : Mealy state action (option out) := + { initial := @initial _ _ _ msync_mealy + ; step := fun s a => if (decide (delayed a s)) + then s + else @step _ _ _ msync_mealy s a + ; output := fun s a => if (decide (delayed a s)) + then None + else Some (@output _ _ _ msync_mealy s a) + }. + + +Class MApi (domain : Type) (API : Type) (state action out : Type) := + { mapi_mealy : Mealy state action out + ; domain_dec :> forall (x y : domain), Decision (x = y) + ; dom_api : API -> domain + ; sem_api : API -> list action + }. + +Definition upd `{MApi domain API s a o} + (f : domain -> list a) a b := + fun d => if (decide (a = d)) then b else f d. + +Global Instance MApi_as_Mealy `{MA: MApi domain API state action out} + : Mealy (state * (domain -> list action)) API (option out) + := + { initial := (@initial _ _ _ mapi_mealy, (λ _,[])) + ; step := fun s a => let (s', f) := s + in let step' := @step _ _ _ mapi_mealy + in match (f (dom_api a)) with + | [] => (s', upd f (dom_api a) (sem_api a)) + | (x::xs) => (step' s' x, upd f (dom_api a) xs) + end + ; output := fun s a => let (s', f) := s + in let output' := @output _ _ _ mapi_mealy + in match (f (dom_api a)) with + | [] => None + | (x::xs) => Some (output' s' x) + end + }. + + diff --git a/MealySync.v b/MealySync.v new file mode 100644 index 0000000..441a142 --- /dev/null +++ b/MealySync.v @@ -0,0 +1,79 @@ +Require Import Rushby. +Require Import base. + +Class MSync (state action out : Type) + := { + msync_mealy : Mealy state action out; + delayed : action -> (state -> Prop); + delayed_dec :> forall a s, Decision (delayed a s) +}. +Check @step. +Instance MSync_as_Mealy `{MSync state action out} + : Mealy state action (option out). +Proof. +split. exact (@initial _ _ _ msync_mealy). +refine (fun s a => if (decide (delayed a s)) + then @step _ _ _ msync_mealy s a + else s). +refine (fun s a => if (decide (delayed a s)) + then Some (@output _ _ _ msync_mealy s a) + else None). +Qed. + +Section MealyM. + +Variable state action out : Type. +Variable MM : MSync state action out. +Variable domain : Type. +Check Policy. +Variable P : Policy domain. +Variable VP : ViewPartition domain. + + +Definition sync_separation `{Policy action domain} := forall (s : state) (b : action) (a : action), + ¬ (delayed a s) ∧ (delayed a (step s a)) + → policy (Rushby.dom b) (Rushby.dom a). + +Definition sync_interf `{Policy action domain} `{MMs : MMsync state action out} + +Class SyncPartition {domain state action out : Type} (MMs : MMsync state action out) {P : Policy domain} {VP : @ViewPartition state domain} := { + sync_partitioned : forall s t a, view_partition (Rushby.dom a) s t -> (delayed a s <-> delayed a t) + }. + + +Section Unwinding. +Context {state action out : Type}. +Context {domain : Type}. +Context {P : @Policy action domain}. +Context {VP : @ViewPartition state domain}. +Context {MMs : MMsync state action out}. +Definition MM := underlyingM. +Definition N := (@MMsync_is_MM domain state action out MMs). + +Context {OC : @OutputConsistent _ _ _ MM domain P VP}. +Context {SP : SyncPartition MMs}. +Instance OC' : @OutputConsistent _ _ _ N domain P VP. +Proof. + intros a s t L. + unfold output; simpl. + destruct (decide (delayed a s)) as [D | ND]; + destruct (decide (delayed a t)) as [D' | ND']; auto; + try (erewrite output_consistent by (apply L); reflexivity); + (exfalso; (apply ND' || apply ND); + (rewrite <- (sync_partitioned s t a L) || + rewrite -> (sync_partitioned s t a L)); auto). +Qed. + +Theorem unwinding_sync : locally_respects_policy (MM:=MM) -> step_consistent (MM:=MM) -> sync_separation -> security (MM:=N). +Proof. intros. +apply unwinding. + +(* local step consistency *) +intros a u s NP. unfold step; simpl. +destruct (decide (delayed a s)); auto. reflexivity. +(* TODO auto cannot solve reflexivity? *) + +intros a s t u L. unfold step; simpl. +destruct (decide (delayed a s)) as [D | ND]; +destruct (decide (delayed a t)) as [D' | ND']; auto. +transitivity t; auto. apply H. apply diff --git a/Monoids.v b/Monoids.v new file mode 100644 index 0000000..912f4eb --- /dev/null +++ b/Monoids.v @@ -0,0 +1,30 @@ +Require Import base. + +Class Monad M {ret : MRet M} {bind : MBind M} := + { ret_unit_1 : forall {A} (m : M A) , m ≫= mret = m + ; ret_unit_2 : forall {A B} (x : A) (f : A → M B), + (mret x) ≫= f = f x + ; bind_assoc : forall {A B C} (m : M A) (f : A → M B) (g : B → M C), + (m ≫= f) ≫= g = m ≫= (fun x => f x ≫= g) + }. + +Global Instance Join_of_Monad M `{Monad M} : (MJoin M) := + fun A (m : M (M A)) => m ≫= id. +Global Instance FMap_of_Monad M `{Monad M} : FMap M := + fun A B f ma => ma ≫= (fun x => mret (f x)). + +Class Monoid A (op: A → A → A) (e : A) := + { op_assoc : Associative (=) op + ; e_left : LeftId (=) e op + ; e_right : RightId (=) e op + }. + +Definition kleisli {A B C} `{mon : Monad M} (f : A → M B) (g : B → M C) (x : A) : M C := y ← f x; g y. +Notation "f >=> g" := (kleisli f g) (at level 60, right associativity) : C_scope. +Notation "( f >=>)" := (kleisli f) (only parsing) : C_scope. +Notation "(>=> g )" := (fun f => kleisli f g) (only parsing) : C_scope. +Notation "(>=>)" := (fun f g => kleisli f g) (only parsing) : C_scope. +Notation "g <=< f" := (kleisli f g) (at level 60, right associativity) : C_scope. +Notation "( g <=<)" := (fun f => kleisli f g) (only parsing) : C_scope. +Notation "(<=< f )" := (kleisli f) (only parsing) : C_scope. + diff --git a/Policy.v b/Policy.v new file mode 100644 index 0000000..fd8af48 --- /dev/null +++ b/Policy.v @@ -0,0 +1,19 @@ +Require Import base. + +Class Policy (action domain : Type) := { + dom : action -> domain; + domain_dec :> forall (x y : domain), Decision (x = y); + policy :> relation domain; + policy_dec :> (forall v w, Decision (policy v w)); + policy_refl :> Reflexive policy +}. + +Infix "⇝" := policy (at level 70). + +Fixpoint purge `{Policy action domain} (ls : list action) (v : domain) : list action := + match ls with + | [] => [] + | a::tl => if (decide (dom a ⇝ v)) then a::(purge tl v) + else purge tl v + end. + diff --git a/Rushby.v b/Rushby.v new file mode 100644 index 0000000..6eee72c --- /dev/null +++ b/Rushby.v @@ -0,0 +1,520 @@ +(** printing -> #→# *) +(** printing (policy a b) #a ⇝ b# *) + +(** Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by J. Rushby + www.csl.sri.com/papers/csl-92-2/ +*) + + +(** We use Robbert Krebbers' prelude, see https://github.com/robbertkrebbers/ch2o/tree/master/prelude **) +Require Import list relations collections fin_collections. +Parameter FinSet : Type -> Type. +(** begin hide **) +Context `{forall A, ElemOf A (FinSet A)}. +Context `{forall A, Empty (FinSet A)}. +Context `{forall A, Singleton A (FinSet A)}. +Context `{forall A, Union (FinSet A)}. +Context `{forall A, Intersection (FinSet A)}. +Context `{forall A, Difference (FinSet A)}. +Context `{forall A, Elements A (FinSet A)}. +Context `{forall A, Collection A (FinSet A)}. (* TODO: i wrote this line down so that there is a Collection -> SimpleCollection -> JoinSemiLattice instance for FinSet; how come this is not automatically picked up by the next assumption? *) +Context `{forall A (H : (forall (a b :A), Decision (a = b))), FinCollection A (FinSet A)}. +(** end hide **) + +(** * Mealy machines *) + +(** A Mealy machine is a state machine with labels and outputs on arrows *) + +Class Mealy (state action out : Type) := { + initial : state; + step : state -> action -> state; + output : state -> action -> out +}. + +(** ** Auxiliary functions + +We define a [run] of a machine [M], which is an extension of +the [step] function to lists of actions. We use a shortcut +[do_actions] for running the machine from the [initial] state. *) + + +Fixpoint run `{Mealy state action out} (s : state) (ls : list action) : state := + match ls with + | nil => s + | a::tl => run (step s a) tl + end. + +Definition do_actions `{Mealy state action out} : list action -> state := run initial. + +(** The [test] function runs the required list of actions and examines the output of the resulting state on a specified action. *) +Definition test `{Mealy state action out} (ls : list action) : action -> out := output (do_actions ls). + +Section Rushby. + +(** We assume for the rest of the formalisation that we have a Mealy +machine [M]. Thus, we parameterize our main development module by a machine [M]. *) + + +Context `{MM : Mealy state action out}. + + +(** * Security policies *) +Section Policy. + +(** In order to define the notion of security, we assume a type [domain] of security domains. Those can be, e.g. clearance levels. For each action [a] we assign a domain [dom a] of that action. For instance, if we interpret domains as clearance levels, the domain of an action can signify the clearance level required to observe/preform the action. + +A *security policy* is defined to be a reflexive decidable relation on the type of domains. For instance, the policy relation can state that the clearance level [u] is below the clearance level [v]. *) +Class Policy (domain : Type) := { + dom : action -> domain; + + (** Sidenote: I had a lot of issues with Coq not finding relevant + typeclass instances because the next field was declared as + [domain_dec : TYPE] instead of [domain_dec :> TYPE]. So we actually + do need implicit coercions to get automatic resolution of typeclass + instances. *) + + domain_dec :> forall (x y : domain), Decision (x = y); + policy :> relation domain; + policy_dec :> (forall v w, Decision (policy v w)); + policy_refl :> Reflexive policy +}. + +(** TODO: Make this notation span over different sections? *) +Delimit Scope policy_scope with P. +Open Scope policy_scope. +Infix "⇝" := policy (at level 70) : policy_scope. + +(** Quoting Rushby: + +<< + We wish to define security in terms of information flow, so the + next step is to capture the idea of the "flow of information" + formally. The key observation is that information can be said to + flow from a domain [u] to a domain [v] exactly when the acions + submitted by domain [u] cause the behavior of the system + percieved by domain [v] to be different from that perceived when + those actions are not present. +>> + +Hence, we define a function [purge] that removes from the given list +all the actions that are not supposed to "influence" the domain [v]. +*) + +Fixpoint purge `{Policy domain} (ls : list action) (v : domain) : list action := + match ls with + | [] => [] + | a::tl => if (decide (dom a ⇝ v)) then a::(purge tl v) + else purge tl v + end. + + +(** Then, the system is _secure_ w.r.t. a given policy if for any set +of actions that can be performed, the system cannot tell the +difference between preforming the given actions and only performing +the actions that are supposed to influence the outcome *) + +Definition security `{Policy domain} := forall (ls : list action) (a : action), + test ls a = test (purge ls (dom a)) a. + + +End Policy. + +(** * View partitions + +As we have seen, the non-interference notion of security is defined by +quantifying over all the possible paths of the system. We wish to +develop techniques for establishing the security property by putting +conditions on individual state transformations. + +As a first step, we define a notion of a "view partition", which is an +equivalence relation on the type of states of the system, siginfying +that two states are "identitcal" or indistinguishable for a given +domain. + +*) + +Section view_partitions. + +(** Formally, a view partition is an assignment of an equivalence +relation [≈{u}] for every domain [u] *) + +Class ViewPartition (domain : Type) := { + view_partition :> domain -> relation state; + view_partition_is_equiv :> forall v, Equivalence (view_partition v) +}. + +Notation "S ≈{ U } T" := (view_partition U S T) + (at level 70, format "S ≈{ U } T") : policy_scope. +Open Scope policy_scope. +(** We say that a system is _output consistent_ if for every two +states [s, t] that are indistinguishable w.r.t. the domain [dom a], +the output of the system [output s a] is the same as [output t a] *) + +Class OutputConsistent `{P : Policy domain} `(ViewPartition domain) := + output_consistent : (forall a s t, s ≈{dom a} t -> output s a = output t a). + +(** Our first lemma states that if we have a view partitioned system +that is output consistent and satisfies + +[[(do_actions ls) ≈{u} (do_actions (purge ls u))]] + +then the system is secure. *) + +(* Lemma 1 *) +Lemma output_consist_security `{P : Policy domain} `{VP : ViewPartition domain} {OC : @OutputConsistent domain P VP} : (forall ls u, + (do_actions ls) ≈{u} (do_actions (purge ls u))) + -> security. +Proof. + intros L ls a. apply output_consistent. + apply (L _ (dom a)). +Qed. + +(** Note that the conditions of Lemma [output_consist_security] still +require us to quantify over all possible paths of the system. We wish +to replace this condition with the following two "local" conditions. + +The first condition, stating that the view partitioned system _locally +respects policy_: if the domain [dom a] is not suppose to interfere +with the domain [u], then, from the point of view of [u], the states +[s] and [step s a] are indistinguishable. +*) + +Definition locally_respects_policy `{Policy domain} `{ViewPartition domain} := forall a u s, + ¬(policy (dom a) u) -> s ≈{u} (step s a). + +(** We say that the system is *step consistent*, if the view partition +is closed under the [step] function. *) + +Definition step_consistent `{Policy domain} `{ViewPartition domain} := forall a s t u, + s ≈{u} t -> (step s a) ≈{u} (step t a). + +(** Given those two conditions we can prove that the system is secure, +by applying the previous lemma *) + +(* Theorem 1 *) +Theorem unwinding `{P: Policy domain} `{VP: ViewPartition domain} `{@OutputConsistent domain P VP} : locally_respects_policy -> step_consistent -> security. +Proof. + intros LRP SC. apply output_consist_security. + assert (forall ls u s t, view_partition u s t -> view_partition u (run s ls) (run t (purge ls u))) as General. (* TODO: a simple generalize would not suffice, because we actually need the s ≈ t assumption *) + induction ls; simpl; auto. + intros u s t HI. + destruct (decide (policy (dom a) u)). + (* DOESNT WORK (Lexer) : destruct (decide ((dom a) ⇝ u)). *) + (** Case [(dom a) ~> u] *) + apply IHls. apply SC; assumption. + (** Case [(dom a) ~/> u] *) + apply IHls. + transitivity s. symmetry. unfold locally_respects_policy in LRP. apply LRP; assumption. assumption. + unfold do_actions. intros ls u. apply General. reflexivity. +Qed. + +End view_partitions. + +(** * Access control interpretation of the view partition. *) + +Section ACI. + +(** In this section we consider a formalisation of the access control mechansisms. + +We say that the machine has _structured state_ if we have a collection +of [name]s and [value]s (the latter being decidable), and some sort of +the memory assigned to each state, which is formally given by the +[contents] function. For each domain [u] we assign sets [observe u] +and [alter u] of names that are allowed to be observed and altered, +respectively, by the domain [u]. *) + +Class StructuredState (domain : Type) := { + name : Type; + value : Type; + contents : state -> name -> value; + value_dec :> forall (v1 v2 : value), Decision (v1 = v2); + observe : domain -> FinSet name; + alter : domain -> FinSet name +}. + +(** This induces the view partition relation as follows: two state [s] +and [t] are indistinguishable for the given domain, if all the +observable contents at [s] is the same as the observable content at +[t] *) + +Definition RMA_partition `{@StructuredState domain} (u : domain) s t := (forall n, (n ∈ observe u) -> contents s n = contents t n). + +Transparent RMA_partition. + +Instance RMA `{@StructuredState domain} : ViewPartition domain := { view_partition := RMA_partition }. +(* begin hide *) + intro u. split; unfold RMA_partition. + (* Reflexivity *) unfold Reflexive. auto. + (* Symmetry *) unfold Symmetric. intros x y Sy. + symmetry. apply Sy. assumption. + (* Transitivity *) unfold Transitive. intros x y z T1 T2 n. + transitivity (contents y n); [apply T1 | apply T2]; assumption. +Defined. (* We have to use 'Defined' here instead of 'Qed' so that we can unfold 'RMA' later on *) +(* end hide *) + +Hint Resolve RMA. + +(** ** Reference monitor assumptions *) +(* TODO: explain those assumptions *) +Class RefMonAssumptions `{Policy domain} `{StructuredState domain} := + { rma1 : forall (a : action) s t, + view_partition (dom a) s t -> output s a = output t a + ; rma2 : forall a s t n, + view_partition (dom a) s t -> + ((contents (step s a) n) ≠ (contents s n) + ∨ (contents (step t a) n) ≠ (contents t n)) + -> contents (step s a) n = contents (step t a) n + ; rma3 : forall a s n, + contents (step s a) n ≠ contents s n -> n ∈ alter (dom a) +}. + +(** If the reference monitor assumptions are satisfied, then the system is output-consistent *) +Global Instance OC `{RefMonAssumptions}: OutputConsistent RMA. +exact rma1. Defined. + +(** The reference mointor assumptions provide the security for the system, if, furthermore, two additional requirements are satisfied: + +- [u ~> v] implies [observe u ⊆ observe v]; that is, if [u] is supposed to interfere with [v], then [v] can observe at least as much as [u] +- if [n ∈ alter u] and [n ∈ observe v], then [u ~> v]; that is, if [u] is allowed to alter a location that is observable by [v], then [u] is allowed to interfere with [v] +*) + +(* Theorem 2 *) +Theorem RMA_secutity `{RefMonAssumptions} : + (forall u v, (policy u v) → observe u ⊆ observe v) + -> (forall u v n, (n ∈ alter u) → (n ∈ observe v) → (policy u v)) + -> security. +Proof. + intros Cond1 Cond2. apply unwinding. + (** We apply the unwinding theorem, so we have to verify that + we locally respect policy and that we have step-consistency *) + unfold locally_respects_policy. + intros a u s. + + (** In order to prove that the system locally respects the policy + relation, we first state the contrapositive, which we can prove + because the policy relation and type of values are decidable *) + + assert ((exists n, (n ∈ observe u ∧ (contents s n ≠ contents (step s a) n))) -> policy (dom a) u) as CP. + intros opH. destruct opH as [n [??]]. + eapply Cond2. eapply rma3. eauto. assumption. + intros NPolicy. + unfold view_partition, RMA, RMA_partition. + (* TODO: why can't decide automatically pick the instance value_dec? *) + intros. destruct (decide (contents s n = contents (step s a) n)) as [e|Ne]. assumption. exfalso. apply NPolicy. apply CP. + exists n; split; assumption. + + (** In order to prove step-consistency we wish to apply the second + reference monitor assumption. For that we must distinguish three + cases: (contents (step s a) n ≠ contents s n), (contents (step t a) + n ≠ contents t n), or if both of the equalities hold *) + intros a s t u A. + unfold view_partition, RMA, RMA_partition in *. + intros n nO. + destruct (decide (contents (step s a) n = contents s n)) as [E1 | NE1]. + destruct (decide (contents (step t a) n = contents t n)) as [E2 | NE2]. + (* Both equalities hold *) + rewrite E1, E2. apply A; assumption. + (* NE2 *) + (* We use the Second RM assmption to deal with this case *) + apply rma2. (* for this we have to show that s ~_(dom a) t *) + unfold view_partition, RMA, RMA_partition. + intros m L. apply A. + apply Cond1 with (u:=dom a). + apply Cond2 with (n:=n); [eapply rma3 | ]; eassumption. + assumption. + right. auto. + (* NE1 case is similar *) + (* TODO: repetition *) + apply rma2. (* for this we have to show that s ~_(dom a) t *) + unfold view_partition, RMA, RMA_partition. + intros m L. apply A. + apply Cond1 with (u:=dom a). + apply Cond2 with (n:=n); [eapply rma3| ]; eassumption. + assumption. + left. auto. +Qed. + +End ACI. + +(** * Intransitive security policy *) +Section Intransitive. + +(** Auxiliary definitions *) +Fixpoint sources `{Policy domain} (ls : list action) (d : domain) : FinSet domain := + match ls with + | [] => {[ d ]} + | a::tl => let src := sources tl d in + if (decide (exists (v: domain), ((v ∈ src) ∧ (policy (dom a) v)))) + then src ∪ {[ dom a ]} else src + end. + +(** The two properties of the [sources] function: it is monotone and [d \in sources ls d] *) +Lemma sources_mon `{Policy} : forall a ls d, sources ls d ⊆ sources (a::ls) d. +Proof. + intros. simpl. + destruct (decide _); [apply union_subseteq_l |]; auto. +Qed. + +Hint Resolve sources_mon. + +Lemma sources_monotone `{Policy} : forall ls js d, ls `sublist` js → sources ls d ⊆ sources js d. +Proof. + intros ls js d M. + induction M. simpl. reflexivity. + simpl. destruct (decide (∃ v : domain, v ∈ sources l1 d ∧ policy (dom x) v)); destruct (decide (∃ v : domain, v ∈ sources l2 d ∧ policy (dom x) v)). + apply union_preserving_r. assumption. + exfalso. apply n. destruct e as [v [e1 e2]]. exists v; split; try (apply (IHM v)); assumption. + transitivity (sources l2 d). assumption. apply union_subseteq_l. + assumption. + transitivity (sources l2 d); auto. +Qed. + +Lemma sources_in `{Policy} : forall ls d, d ∈ sources ls d. +Proof. + intros. induction ls; simpl. apply elem_of_singleton_2; auto. + destruct (decide (∃ v : domain, v ∈ sources ls d ∧ policy (dom a) v)); simpl. + apply elem_of_union_l. assumption. assumption. +Qed. + +Hint Resolve sources_in. + +Fixpoint ipurge `{Policy} (ls : list action) (d : domain) := + match ls with + | [] => [] + | a::tl => if (decide ((dom a) ∈ sources ls d)) + then a::(ipurge tl d) + else ipurge tl d + end. + +(** The non-interference notion of security for intransitive policies +is very similar to the transitive case, bu uses the [ipurge] function +instead of [purge] *) + +Definition isecurity `{Policy} := forall ls a, + test ls a = test (ipurge ls (dom a)) a. + +(** We can prove lemmas similar to the transitive case *) + +Lemma output_consist_isecurity `{P : Policy domain} `{VP : ViewPartition domain} {OC : @OutputConsistent domain P VP} : (forall ls u, + view_partition u (do_actions ls) (do_actions (ipurge ls u))) + -> isecurity. +Proof. + unfold isecurity. intros H ls a. + unfold test. + apply output_consistent. + apply (H ls (dom a)). +Qed. + +Definition view_partition_general `{ViewPartition domain} (C : FinSet domain) s t := forall (u: domain), u ∈ C -> view_partition u s t. + +Global Instance view_partition_general_equiv `{ViewPartition domain}: + forall V, Equivalence (view_partition_general V). +Proof. + intro V. split. + intros x v A. reflexivity. + intros x y A1 v A2. symmetry. apply (A1 v); assumption. + intros x y z A1 A2 v A3. transitivity y. apply (A1 v); assumption. apply (A2 v); assumption. +Qed. + +Definition weakly_step_consistent `{Policy domain} `{ViewPartition domain} := + forall s t u a, view_partition u s t -> view_partition (dom a) s t -> view_partition u (step s a) (step t a). + +Ltac exists_inside v := + let H := fresh "Holds" in + let nH := fresh "notHolds" in + destruct (decide _) as [H | []]; + [ try reflexivity | exists v; try auto]. + +Local Hint Resolve sources_mon. +Local Hint Extern 1 (_ ∈ sources (_::_) _) => eapply sources_mon. +Local Hint Immediate elem_of_singleton. +(* Local Hint Extern 1 (_ ∈ {[ _ ]}) => apply elem_of_singleton; trivial. *) +Local Hint Resolve elem_of_union. + +(* Lemma 3 *) +Lemma weakly_step_consistent_general `{Policy domain} `{ViewPartition domain} (s t : state) (a : action) ls (u: domain) : weakly_step_consistent -> locally_respects_policy -> + view_partition_general (sources (a::ls) u) s t + -> view_partition_general (sources ls u) (step s a) (step t a). +Proof. + intros WSC LRP P v vIn. + unfold view_partition_general in P. + unfold locally_respects_policy in LRP. + destruct (decide (policy (dom a) v)). + (* Case [dom a ~> v] *) + apply WSC; apply P. auto. + (* we need to show that [dom a ∈ sources (a::ls) v] *) + simpl. exists_inside v. apply elem_of_union. right. auto. apply elem_of_singleton; trivial. + (* Case [dom a ~/> v] *) + transitivity s. symmetry. apply LRP; assumption. + transitivity t. apply P. auto. + apply LRP; assumption. +Qed. + +(* Lemma 4 *) +Lemma locally_respects_gen `{Policy domain} `{ViewPartition domain} (WSC: weakly_step_consistent) (LRP : locally_respects_policy) s a ls u : + ¬ ((dom a) ∈ sources (a::ls) u) -> + view_partition_general (sources ls u) s (step s a). +Proof. + intros domN v vIn. + apply LRP. intro. + (* If [dom a ~> v], then [dom a ∈ sources (a::ls) u], because [v ∈ sources ls u] *) (* again, a clusterfuck *) + apply domN. simpl. + exists_inside v; auto. apply elem_of_union; right; apply elem_of_singleton; reflexivity. +Qed. + + +(* Lemma 5 *) +Lemma unwinding_gen `{Policy domain} `{ViewPartition domain} (WSC: weakly_step_consistent) (LRP : locally_respects_policy) s t ls u : + view_partition_general (sources ls u) s t + -> view_partition u (run s ls) (run t (ipurge ls u)). +Proof. + generalize dependent s. + generalize dependent t. + induction ls; intros s t. + simpl. intro A. apply (A u). apply elem_of_singleton; reflexivity. + intro VPG. simpl. unfold sources. fold (sources (a::ls) u). + + destruct (decide _). + (** Case [dom a ∈ sources (a::ls) u] *) + simpl. apply IHls. apply weakly_step_consistent_general; auto. + (** Case [dom a ∉ sources (a::ls) u] *) + apply IHls. symmetry. transitivity t. + - intros v vIn. symmetry. apply VPG. apply sources_mon; exact vIn. + - apply locally_respects_gen; try(assumption). +Qed. + + +Theorem unwinding_intrans `{P : Policy domain} `{VP : ViewPartition domain} + `{OC : @OutputConsistent domain P VP} (WSC : weakly_step_consistent) (LRP : locally_respects_policy) : isecurity. +Proof. + apply output_consist_isecurity. + intros. + apply unwinding_gen; try assumption. + reflexivity. +Qed. + +Theorem rma_secure_intransitive `{RefMonAssumptions} : (forall u v n, n ∈ alter u -> n ∈ observe v -> policy u v) -> isecurity. +Proof. intro policyA. + apply @unwinding_intrans with (VP:=RMA). exact rma1. + intros s t u a A1 A2. + unfold view_partition. unfold RMA_partition; simpl. intros n L. + destruct (decide (contents (step s a) n = contents s n)) as [E1 | NE1]. + destruct (decide (contents (step t a) n = contents t n)) as [E2 | NE2]. + (* Case [contents (step s a) n = contents s n /\ contents (step t a) n = contents t n] *) + rewrite E1, E2. apply A1; assumption. + (* Case [contents (step t a) n ≠ contents t n] *) + apply rma2; [ | right]; assumption. + (* Case [contents (step s a) n ≠ contents s n] *) + apply rma2; [ | left]; assumption. + + intros a u s A. + assert ((exists n, (n ∈ observe u ∧ (contents s n ≠ contents (step s a) n))) -> policy (dom a) u) as CP. + intros opH. destruct opH as [n [??]]. + eapply policyA. eapply rma3. eauto. assumption. + intros n L. destruct (decide (contents s n = contents (step s a) n)). assumption. exfalso. apply A. + apply CP. exists n. auto. +Qed. + +End Intransitive. + +End Rushby. diff --git a/Security.v b/Security.v new file mode 100644 index 0000000..7d7e118 --- /dev/null +++ b/Security.v @@ -0,0 +1,184 @@ +(* rewrite using the view partition relation +TODO *) + +Require Import base. +Require Import Mealy. +Require Import Policy. +Require Import ViewPartition. + +Class IsSecure {domain : Type} + `(M : Mealy state action out) + (P : Policy action domain) := + noninterference : + (forall (ls : list action) (a : action), test ls a = test (purge ls (dom a)) a). + +Section MealySec. + Variable (state action out : Type). + Variable (M : Mealy state action out). + Variable domain : Type. + Variable (P : Policy action domain). + Variable (VP : ViewPartition M domain). + Lemma output_consist_view_security {OC : OutputConsistent P VP} : (forall ls u, + (do_actions ls) ≈{u} (do_actions (purge ls u))) + -> IsSecure M P. + Proof. + intros L ls a. apply output_consistent. + apply (L _ (dom a)). + Qed. + +Instance unwinding {OC : OutputConsistent P VP} {LRP : LocallyRespectsPolicy P VP} {SC: StepConsistent P VP} : IsSecure M P. +Proof. + apply output_consist_view_security. + assert (forall ls v s t, view_partition v s t -> view_partition v (run s ls) (run t (purge ls v))) as General. (* TODO: a simple generalize would not suffice, because we actually need the s ≈ t assumption *) + induction ls; simpl; auto. + intros u s t HI. + destruct (decide (policy (dom a) u)). + (* DOESNT WORK (Lexer) : destruct (decide ((dom a) ⇝ u)). *) + (** Case [(dom a) ~> u] *) + eapply IHls. apply step_consistent. assumption. + (** Case [(dom a) ~/> u] *) + eapply IHls. + transitivity s; [| assumption]. symmetry. apply locally_respects_policy. assumption. + unfold do_actions. intros ls u. eapply General; reflexivity. +Qed. + +Instance unwinding_trans {OC : OutputConsistent P VP} {LRP : LocallyRespectsPolicy P VP} {TP: Transitive policy} {SC: WeakStepConsistent P VP} : IsSecure M P. +Proof. + apply output_consist_view_security. + assert (forall ls u s t, (forall v, policy v u -> view_partition v s t) -> (forall v, policy v u -> view_partition v (run s ls) (run t (purge ls v)))) as General. + induction ls; simpl; auto. + intros u s t S v HI. + destruct (decide (policy (dom a) v)). + (** Case [(dom a) ~> u] *) + apply IHls with (u:=u); try assumption. + intros v' Hv'. + apply weak_step_consistent; apply S. etransitivity; eassumption. + assumption. + (** Case [(dom a) ~/> u] *) + apply IHls with (u:=v); try assumption. + intros v' Hv'. + transitivity s. symmetry. + apply locally_respects_policy. intro. + apply n. rewrite H. assumption. + apply S. rewrite Hv'. assumption. reflexivity. + unfold do_actions. intros ls u. eapply General; reflexivity. +Qed. + +End MealySec. + +Module MSyncSec. + Variable (state action out : Type). + Variable (M : MSync state action out). + Definition M' : Mealy state action out := msync_mealy. + Variable domain : Type. + Variable (P : Policy action domain). + Variable (VP' : ViewPartition M' domain). + + Instance VP: ViewPartition (MSync_as_Mealy (MS:=M)) domain + := + { view_partition := @view_partition _ _ _ _ _ VP' + ; view_partition_is_equiv := @view_partition_is_equiv _ _ _ _ _ VP' + }. + + Class SyncPartitioned := + { sync_partitioned : forall s t a, view_partition (dom a) s t -> (delayed a s <-> delayed a t) + }. + + + Global Instance oc2 {SP: SyncPartitioned} (OC: OutputConsistent P VP') : + OutputConsistent P VP. + Proof. + intros a s t L. + unfold output; simpl. + destruct (decide (delayed a s)) as [D | ND]; + destruct (decide (delayed a t)) as [D' | ND']; + try solve + [erewrite output_consistent by (apply L); + reflexivity | reflexivity ]. + exfalso. apply ND'. rewrite <- (sync_partitioned s t a L). assumption. + exfalso. apply ND. rewrite -> (sync_partitioned s t a L). assumption. + Qed. + +Theorem unwinding_sync_trans {SP: SyncPartitioned} {OC : OutputConsistent P VP'} {LRP : LocallyRespectsPolicy P VP'} {TP : Transitive policy} {SC: WeakStepConsistent P VP'} : IsSecure (MSync_as_Mealy (MS:=M)) P. +Proof. +intros. +apply unwinding_trans with (VP:=VP). (* TODO: i want this to be resolved automatically *) apply oc2. assumption. + +(* Locally respects policy *) +intros a u s NP. unfold step; simpl. +destruct (decide (delayed a s)); auto. reflexivity. + +(* Transitive policy *) assumption. (* again, can this be picked up automatically? *) + +(* Step-consitency *) +intros a s t u Ldom L. unfold step; simpl. +destruct (decide (delayed a s)) as [D | ND]; +destruct (decide (delayed a t)) as [D' | ND']; +try assumption. +(* only s is delayed by a *) +exfalso. apply ND'. rewrite sync_partitioned; try eassumption. +symmetry; assumption. +(* similar case, but symmetric *) +exfalso. apply ND. rewrite sync_partitioned; try eassumption. +(* both s and t are delayed by a *) +eapply weak_step_consistent; assumption. +Qed. + +End MSyncSec. + +Module MApiSec. + Variable (state action out : Type). + Variable domain : Type. + Variable API : Type. + Variable (P : Policy API domain). + Variable (M : MApi domain API state action out). + Definition M' : Mealy state action out := mapi_mealy. + Variable (VP' : ViewPartition M' domain). + + Definition vpeq : domain -> relation (state * (domain -> list action)) := fun d s1 s2 => + let (s1', f) := s1 + in let (s2', g) := s2 + in @view_partition _ _ _ _ _ VP' d s1' s2' /\ f = g. + + Lemma vpeq_eq (d : domain) : Equivalence (vpeq d). + Proof. + intros. split; unfold vpeq. + intros [s ?]. split; reflexivity. + + intros [s ?] [t ?] [? ?]. split; symmetry; auto. + + intros [s ?] [t ?] [z ?] [? ?] [? ?]. split; etransitivity; eassumption. + Qed. + + Instance VP: ViewPartition (MApi_as_Mealy (MA:=M)) domain + := + { view_partition := vpeq + ; view_partition_is_equiv := vpeq_eq + }. + + Instance: IsSecure (MApi_as_Mealy (MA:=M)) P. + Proof. intros. apply unwinding_trans with (VP:=VP). + + (* output consistency *) + intro. intros [s f] [t g]. + simpl. + remember (f (dom_api a)) as L1; + remember (g (dom_api a)) as L2. + destruct L1; + destruct L2; try (subst; reflexivity). + + intros [? Z]. exfalso. rewrite Z in *. + rewrite <- HeqL2 in *. + inversion HeqL1. + + intros [? Z]. exfalso. rewrite Z in *. + rewrite <- HeqL2 in *. + inversion HeqL1. + + intros [? Z]. f_equal. + rewrite Z in *. + rewrite <- HeqL1 in *. + inversion HeqL2. + apply output_consistency. + (* TODO replace dom in policy with the Dom class *) +End MApiSec. diff --git a/ViewPartition.v b/ViewPartition.v new file mode 100644 index 0000000..4f08cd6 --- /dev/null +++ b/ViewPartition.v @@ -0,0 +1,29 @@ +Require Import base. +Require Import Policy. +Require Import Mealy. +(** Formally, a view partition is an assignment of an equivalence +relation [≈{u}] for every domain [u] *) + +Class ViewPartition `(M : Mealy state action out) (domain : Type) := { + view_partition :> domain -> relation state; + view_partition_is_equiv :> forall v, Equivalence (view_partition v) +}. + +Notation "S ≈{ U } T" := (view_partition U S T) + (at level 70, format "S ≈{ U } T"). + +Class OutputConsistent {domain : Type} `{M : Mealy state action out} + (P : Policy action domain) (VP: ViewPartition M domain) := + output_consistent : (forall a s t, s ≈{dom a} t -> output s a = output t a). + +Class LocallyRespectsPolicy {domain : Type} `{M : Mealy state action out} + (P : Policy action domain) (VP: ViewPartition M domain) := + locally_respects_policy : (forall a u s, ¬(policy (dom a) u) -> s ≈{u} (step s a)). + +Class WeakStepConsistent {domain : Type} `{M : Mealy state action out} + (P : Policy action domain) (VP: ViewPartition M domain) := + weak_step_consistent : (forall a s t u, s ≈{dom a} t -> s ≈{u} t -> (step s a) ≈{u} (step t a)). + +Class StepConsistent {domain : Type} `{M : Mealy state action out} + (P : Policy action domain) (VP: ViewPartition M domain) := + step_consistent : (forall a s t u, s ≈{u} t -> (step s a) ≈{u} (step t a)).