diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 47 | ||||
| -rw-r--r-- | theories/Program/FunctionalExtensionality.v | 12 | ||||
| -rw-r--r-- | theories/Program/Program.v | 1 | ||||
| -rw-r--r-- | theories/Program/Subset.v | 141 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 24 | ||||
| -rw-r--r-- | theories/Program/Utils.v | 18 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 16 |
7 files changed, 209 insertions, 50 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 96c1c8f4d..85ed18891 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -85,17 +85,6 @@ Ltac abstract_eq_hyp H' p := end end. -(** Try to abstract a proof of equality, if no proof of the same equality is present in the context. *) - -Ltac abstract_any_hyp H' p := - match type of p with - ?X => - match goal with - | [ H : X |- _ ] => fail 1 - | _ => set (H':=p) ; try (change p with H') ; clearbody H' ; simpl in H' - end - end. - (** Apply the tactic tac to proofs of equality appearing as coercion arguments. Just redefine this tactic (using [Ltac on_coerce_proof tac ::=]) to handle custom coercion operators. *) @@ -180,3 +169,39 @@ Ltac clear_eqs := repeat clear_eq. Ltac simplify_eqs := simpl ; simpl_eqs ; clear_eq_ctx ; clear_refl_eqs ; try subst ; simpl ; repeat simpl_uip ; rewrite_refl_id. + +(** A tactic to remove trivial equality guards in hypotheses. *) + +Ltac simpl_IH_eq H := + let tac H' := clear H ; rename H' into H in + let H' := fresh "H" in + match type of H with + | JMeq _ _ -> _ => + assert (H' := H (JMeq_refl _)) ; tac H' + | _ = _ -> _ => + assert (H' := H (refl_equal _)) ; tac H' + end. + +Ltac simpl_IH_eqs H := repeat simpl_IH_eq H. + +Ltac simpl_IHs_eqs := + match goal with + | [ H : JMeq _ _ -> _ |- _ ] => simpl_IH_eqs H + | [ H : _ = _ -> _ |- _ ] => simpl_IH_eqs H + end. + +Require Import Coq.Program.Tactics. + +(** The following tactics allow to do induction on an already instantiated inductive predicate + by first generalizing it and adding the proper equalities to the context, in a maner similar to + the BasicElim tactic of "Elimination with a motive" by Conor McBride. *) + +Tactic Notation "dependent" "induction" ident(H) := + generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; + induction H ; intros ; subst* ; try discriminates ; try simpl_IHs_eqs. + +(** This tactic also generalizes the goal by the given variables before the induction. *) + +Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := + generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; + generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates ; try simpl_IHs_eqs. diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v index 22cb93d56..382252ce2 100644 --- a/theories/Program/FunctionalExtensionality.v +++ b/theories/Program/FunctionalExtensionality.v @@ -48,13 +48,13 @@ Ltac apply_ext := (** For a function defined with Program using a well-founded order. *) -Lemma fix_sub_eq_ext : +Program Lemma fix_sub_eq_ext : forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) (P : A -> Set) - (F_sub : forall x : A, (forall {y : A | R y x}, P (`y)) -> P x), + (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x), forall x : A, Fix_sub A R Rwf P F_sub x = - F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)). + F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y). Proof. intros ; apply Fix_eq ; auto. intros. @@ -65,12 +65,12 @@ Qed. (** For a function defined with Program using a measure. *) -Lemma fix_sub_measure_eq_ext : +Program Lemma fix_sub_measure_eq_ext : forall (A : Type) (f : A -> nat) (P : A -> Type) - (F_sub : forall x : A, (forall {y : A | f y < f x}, P (`y)) -> P x), + (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x), forall x : A, Fix_measure_sub A f P F_sub x = - F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)). + F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y). Proof. intros ; apply Fix_measure_eq ; auto. intros. diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 39c5b7734..fb172db84 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -1,3 +1,4 @@ Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. Require Export Coq.Program.Equality. +Require Export Coq.Program.Subset. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v new file mode 100644 index 000000000..54d830c89 --- /dev/null +++ b/theories/Program/Subset.v @@ -0,0 +1,141 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Coq.Program.Utils. +Require Import Coq.Program.Equality. + +(** Tactics related to subsets and proof irrelevance. *) + +(** Simplify dependent equality using sigmas to equality of the codomains if possible. *) + +Ltac simpl_existT := + match goal with + [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => + let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H + end. + +Ltac simpl_existTs := repeat simpl_existT. + +(** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to + factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *) + +Ltac on_subset_proof_aux tac T := + match T with + | context [ exist ?P _ ?p ] => try on_subset_proof_aux tac P ; tac p + end. + +Ltac on_subset_proof tac := + match goal with + [ |- ?T ] => on_subset_proof_aux tac T + end. + +Ltac abstract_any_hyp H' p := + match type of p with + ?X => + match goal with + | [ H : X |- _ ] => fail 1 + | _ => set (H':=p) ; try (change p with H') ; clearbody H' + end + end. + +Ltac abstract_subset_proof := + on_subset_proof ltac:(fun p => let H := fresh "eqH" in abstract_any_hyp H p ; simpl in H). + +Ltac abstract_subset_proofs := repeat abstract_subset_proof. + +Ltac pi_subset_proof_hyp p := + match type of p with + ?X => + match goal with + | [ H : X |- _ ] => + match p with + | H => fail 2 + | _ => rewrite (proof_irrelevance X p H) + end + | _ => fail " No hypothesis with same type " + end + end. + +Ltac pi_subset_proof := on_subset_proof pi_subset_proof_hyp. + +Ltac pi_subset_proofs := repeat pi_subset_proof. + +(** Clear duplicated hypotheses *) + +Ltac clear_dup := + match goal with + | [ H : ?X |- _ ] => + match goal with + | [ H' : X |- _ ] => + match H' with + | H => fail 2 + | _ => clear H' || clear H + end + end + end. + +Ltac clear_dups := repeat clear_dup. + +(** The two preceding tactics in sequence. *) + +Ltac clear_subset_proofs := + abstract_subset_proofs ; simpl in * |- ; pi_subset_proofs ; clear_dups. + +Ltac pi := repeat progress f_equal ; apply proof_irrelevance. + +Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> (`n) = (`m). +Proof. + induction n. + induction m. + simpl. + split ; intros ; subst. + + inversion H. + reflexivity. + + pi. +Qed. + +(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] + in tactics. *) + +Program Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B := + fn (exist _ x (refl_equal x)). + +(* This is what we want to be able to do: replace the originaly matched object by a new, + propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *) + +Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B) + (y : A | y = x), + match_eq A B x fn = fn y. +Proof. + intros. + unfold match_eq. + f_equal. + destruct y. + (* uses proof-irrelevance *) + apply <- subset_eq. + symmetry. assumption. +Qed. + +(** Now we make a tactic to be able to rewrite a term [t] which is applied to a [match_eq] using an arbitrary + equality [t = u], and [u] is now the subject of the [match]. *) + +Ltac rewrite_match_eq H := + match goal with + [ |- ?T ] => + match T with + context [ match_eq ?A ?B ?t ?f ] => + rewrite (match_eq_rewrite A B t f (exist _ _ (sym_eq H))) + end + end. + +(** Otherwise we can simply unfold [match_eq] and the term trivially reduces to the original definition. *) + +Ltac simpl_match_eq := unfold match_eq ; simpl. + diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index e4c60e14a..ac0f5cf71 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -50,6 +50,7 @@ Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H]. (** Discriminate that also work on a [x <> x] hypothesis. *) + Ltac discriminates := match goal with | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity @@ -151,21 +152,12 @@ Ltac bang := Tactic Notation "contradiction" "by" constr(t) := let H := fresh in assert t as H by auto with * ; contradiction. -(** The following tactics allow to do induction on an already instantiated inductive predicate - by first generalizing it and adding the proper equalities to the context, in a manner similar to - the BasicElim tactic of "Elimination with a motive" by Conor McBride. *) - -Tactic Notation "dependent" "induction" ident(H) := - generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; - induction H ; intros ; subst* ; try discriminates. - -(** This tactic also generalizes the goal by the given variables before the induction. *) - -Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := - generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; - generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates. +(** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto with *] + is overkill and slows things down, better rebind using [Obligations Tactic := tac] in this case, + possibly using [program_simplify] to use standard goal-cleaning tactics. *) -(** The default simplification tactic used by Program. *) +Ltac program_simplify := + simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; + try (solve [ red ; intros ; destruct_conjs ; discriminate ]). -Ltac program_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; - try (solve [ red ; intros ; destruct_conjs ; discriminate ]) ; auto with *. +Ltac program_simpl := program_simplify ; auto with *. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index a268f0afb..6af81a410 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -18,9 +18,9 @@ Notation " {{ x }} " := (tt : { y : unit | x }). (** A simpler notation for subsets defined on a cartesian product. *) -Notation "{ ( x , y ) : A | P }" := - (sig (fun anonymous : A => let (x,y) := anonymous in P)) - (x ident, y ident) : type_scope. +(* Notation "{ ( x , y ) : A | P }" := *) +(* (sig (fun anonymous : A => let (x,y) := anonymous in P)) *) +(* (x ident, y ident, at level 10) : type_scope. *) (** Generates an obligation to prove False. *) @@ -45,13 +45,13 @@ Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70). (** Quantifying over subsets. *) -Notation "'fun' { x : A | P } => Q" := - (fun x:{x:A|P} => Q) - (at level 200, x ident, right associativity). +(* Notation "'fun' ( x : A | P ) => Q" := *) +(* (fun (x :A|P} => Q) *) +(* (at level 200, x ident, right associativity). *) -Notation "'forall' { x : A | P } , Q" := - (forall x:{x:A|P}, Q) - (at level 200, x ident, right associativity). +(* Notation "'forall' ( x : A | P ), Q" := *) +(* (forall (x : A | P), Q) *) +(* (at level 200, x ident, right associativity). *) Require Import Coq.Bool.Sumbool. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 55784671f..70b1b1b5a 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -34,11 +34,11 @@ Section Well_founded. Hypothesis F_ext : forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)), - (forall y:{ y:A | R y x}, f y = g y) -> F_sub x f = F_sub x g. + (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g. Lemma Fix_F_eq : forall (x:A) (r:Acc R x), - F_sub x (fun (y:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r. + F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r. Proof. destruct r using Acc_inv_dep; auto. Qed. @@ -52,7 +52,7 @@ Section Well_founded. rewrite (proof_irrelevance (Acc R x) r s) ; auto. Qed. - Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{y:A|R y x}) => Fix (proj1_sig y)). + Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:A|R y x) => Fix (proj1_sig y)). Proof. intro x; unfold Fix in |- *. rewrite <- (Fix_F_eq ). @@ -64,7 +64,7 @@ Section Well_founded. forall x : A, Fix_sub P F_sub x = let f_sub := F_sub in - f_sub x (fun {y : A | R y x}=> Fix (`y)). + f_sub x (fun (y : A | R y x) => Fix (`y)). exact Fix_eq. Qed. @@ -98,7 +98,7 @@ Section Well_founded_measure. Section FixPoint. Variable P : A -> Type. - Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. + Variable F_sub : forall x:A, (forall (y : A | m y < m x), P (proj1_sig y)) -> P x. Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *) @@ -106,8 +106,8 @@ Section Well_founded_measure. Hypothesis F_ext : - forall (x:A) (f g:forall y:{y:A | m y < m x}, P (`y)), - (forall y:{ y:A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g. + forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)), + (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g. Lemma Fix_measure_F_eq : forall (x:A) (r:Acc lt (m x)), @@ -137,7 +137,7 @@ Section Well_founded_measure. forall x : A, Fix_measure_sub P F_sub x = let f_sub := F_sub in - f_sub x (fun {y : A | m y < m x}=> Fix_measure (`y)). + f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)). exact Fix_measure_eq. Qed. |