diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-25 20:25:06 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-25 20:25:06 +0000 |
commit | e3535ade2bd4c7b75ec093e9e0f124f84c506b8f (patch) | |
tree | e6ace79e3a52db095645cce68450593758da89e4 /theories/Program | |
parent | b103459011e65c09d481bdaee5fd7ce7638fb139 (diff) |
Various little improvements:
- A new [dependent pattern] tactic to do a pattern on an object in an
inductive family and generalize by both the indexes and the object
itself. Useful to prepare a goal for elimination with a dependent
principle.
- Better dependent elimination simplification tactic that doesn't
throw away non-dependent equalities if they can't be injected.
- Add [fold_sub] and [unfold_sub] tactics for folding/unfolding
well-founded definitions using measures built by Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11420 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Equality.v | 9 | ||||
-rw-r--r-- | theories/Program/FunctionalExtensionality.v | 18 |
2 files changed, 21 insertions, 6 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 2b914ace7..d37fd62f6 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -359,9 +359,9 @@ Definition block_dep_elim {A : Type} (a : A) := a. Ltac simplify_one_dep_elim_term c := match c with - | @JMeq ?A ?a ?A ?b -> _ => refine (simplification_heq _ _ _ _ _) + | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _) | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _) - | eq (existT ?P ?p _) (existT ?P ?p _) -> _ => refine (simplification_existT _ _ _ _ _ _ _) + | eq (existT _ _ _) (existT _ _ _) -> _ => refine (simplification_existT _ _ _ _ _ _ _) | ?x = ?y -> _ => (* variables case *) (let hyp := fresh in intros hyp ; move dependent hyp before x ; @@ -370,11 +370,12 @@ Ltac simplify_one_dep_elim_term c := move dependent hyp before y ; generalize dependent y ; refine (solution_right _ _ _ _) ; intros until 0) | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P) - | ?f ?x = ?g ?y -> _ => let H := fresh in intros H ; injection H ; clear H + | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H) | ?t = ?u -> _ => let hyp := fresh in intros hyp ; elimtype False ; discriminate | ?x = ?y -> _ => let hyp := fresh in - intros hyp ; case hyp ; clear hyp + intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ; + case hyp ; clear hyp | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *) | _ => intro end. diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v index 440217bfe..8bd2dfb90 100644 --- a/theories/Program/FunctionalExtensionality.v +++ b/theories/Program/FunctionalExtensionality.v @@ -22,7 +22,7 @@ Require Import Coq.Program.Equality. Set Implicit Arguments. Unset Strict Implicit. -(** The converse of functional equality. *) +(** The converse of functional extensionality. *) Lemma equal_f : forall A B : Type, forall (f g : A -> B), f = g -> forall x, f x = g x. @@ -32,7 +32,7 @@ Proof. auto. Qed. -(** Statements of functional equality for simple and dependent functions. *) +(** Statements of functional extensionality for simple and dependent functions. *) Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x), @@ -106,4 +106,18 @@ Proof. rewrite H0 ; auto. Qed. +(** Tactics to fold/unfold definitions based on [Fix_measure_sub]. *) +Ltac fold_sub f := + match goal with + | [ |- ?T ] => + match T with + appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => + let app := context C [ f arg ] in + change app + end + end. + +Ltac unfold_sub f fargs := + set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; + rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig. |