From 855ac3eff49e294fd1d2a1c5d039376d706b0f34 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 14 Feb 2018 12:55:20 +0100 Subject: [PATCH] Initial import from darcs --- .gitignore | 14 + ArrayMachine.v | 128 ++ LibTactics.v | 5004 +++++++++++++++++++++++++++++++++++++++++++++++ Libs.v | 80 + Mealy.v | 99 + MealySync.v | 79 + Monoids.v | 30 + Policy.v | 19 + Rushby.v | 520 +++++ Security.v | 184 ++ ViewPartition.v | 29 + 11 files changed, 6186 insertions(+) create mode 100644 .gitignore create mode 100644 ArrayMachine.v create mode 100755 LibTactics.v create mode 100755 Libs.v create mode 100644 Mealy.v create mode 100644 MealySync.v create mode 100644 Monoids.v create mode 100644 Policy.v create mode 100644 Rushby.v create mode 100644 Security.v create mode 100644 ViewPartition.v 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)).