diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 39 | ||||
| -rw-r--r-- | theories/Program/FunctionalExtensionality.v | 31 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 6 | ||||
| -rw-r--r-- | theories/Program/Utils.v | 14 |
4 files changed, 67 insertions, 23 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index e67d32286e..96c1c8f4d1 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -75,11 +75,24 @@ Ltac simpl_eq := simpl ; repeat (elim_eq_rect ; simpl) ; repeat (simpl_uip ; sim (** Try to abstract a proof of equality, if no proof of the same equality is present in the context. *) Ltac abstract_eq_hyp H' p := + let ty := type of p in + let tyred := eval simpl in ty in + match tyred with + ?X = ?Y => + match goal with + | [ H : X = Y |- _ ] => fail 1 + | _ => set (H':=p) ; try (change p with H') ; clearbody H' ; simpl in H' + 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 = ?Y => + ?X => match goal with - | [ H : X = Y |- _ ] => fail 1 - | _ => set (H':=p) ; try (change p with H') ; clearbody H' + | [ H : X |- _ ] => fail 1 + | _ => set (H':=p) ; try (change p with H') ; clearbody H' ; simpl in H' end end. @@ -87,17 +100,19 @@ Ltac abstract_eq_hyp H' p := Just redefine this tactic (using [Ltac on_coerce_proof tac ::=]) to handle custom coercion operators. *) -Ltac on_coerce_proof tac := +Ltac on_coerce_proof tac T := + match T with + | context [ eq_rect _ _ _ _ ?p ] => tac p + end. + +Ltac on_coerce_proof_gl tac := match goal with - [ |- ?T ] => - match T with - | context [ eq_rect _ _ _ _ ?p ] => tac p - end + [ |- ?T ] => on_coerce_proof tac T end. (** Abstract proofs of equalities of coercions. *) -Ltac abstract_eq_proof := on_coerce_proof ltac:(fun p => let H := fresh "eqH" in abstract_eq_hyp H p). +Ltac abstract_eq_proof := on_coerce_proof_gl ltac:(fun p => let H := fresh "eqH" in abstract_eq_hyp H p). Ltac abstract_eq_proofs := repeat abstract_eq_proof. @@ -105,7 +120,9 @@ Ltac abstract_eq_proofs := repeat abstract_eq_proof. in the goal become convertible. *) Ltac pi_eq_proof_hyp p := - match type of p with + let ty := type of p in + let tyred := eval simpl in ty in + match tyred with ?X = ?Y => match goal with | [ H : X = Y |- _ ] => @@ -119,7 +136,7 @@ Ltac pi_eq_proof_hyp p := (** Factorize proofs of equality appearing as coercion arguments. *) -Ltac pi_eq_proof := on_coerce_proof pi_eq_proof_hyp. +Ltac pi_eq_proof := on_coerce_proof_gl pi_eq_proof_hyp. Ltac pi_eq_proofs := repeat pi_eq_proof. diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v index 40356a9c49..22cb93d56b 100644 --- a/theories/Program/FunctionalExtensionality.v +++ b/theories/Program/FunctionalExtensionality.v @@ -11,16 +11,38 @@ Proof. auto. Qed. +(** Eta expansion *) + +Axiom eta_expansion_dep : forall A (B : A -> Type) (f : forall x : A, B x), + f = fun x => f x. + +Lemma eta_expansion : forall A B (f : A -> B), + f = fun x => f x. +Proof. + intros ; apply eta_expansion_dep. +Qed. + (** Statements of functional equality for simple and dependent functions. *) -Axiom fun_extensionality : forall A B (f g : A -> B), +Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), + forall (f g : forall x : A, B x), (forall x, f x = g x) -> f = g. -Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), forall (f g : forall x : A, B x), +Lemma fun_extensionality : forall A B (f g : A -> B), (forall x, f x = g x) -> f = g. +Proof. + intros ; apply fun_extensionality_dep. + assumption. +Qed. Hint Resolve fun_extensionality fun_extensionality_dep : program. +(** Unification needs help sometimes... *) +Ltac apply_ext := + match goal with + [ |- ?x = ?y ] => apply (@fun_extensionality _ _ x y) + end. + (** The two following lemmas allow to unfold a well-founded fixpoint definition without restriction using the functional extensionality axiom. *) @@ -57,9 +79,4 @@ Proof. rewrite H0 ; auto. Qed. -Ltac apply_ext := - match goal with - [ |- ?x = ?y ] => apply (@fun_extensionality _ _ x y) - end. - diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index dfe8453d10..e4c60e14af 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -79,6 +79,9 @@ Ltac on_call f tac := match goal with | H : ?T |- _ => match T with + | context [f ?x ?y ?z ?w ?v ?u ?a ?b ?c] => tac (f x y z w v u a b c) + | context [f ?x ?y ?z ?w ?v ?u ?a ?b] => tac (f x y z w v u a b) + | context [f ?x ?y ?z ?w ?v ?u ?a] => tac (f x y z w v u a) | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) | context [f ?x ?y ?z ?w] => tac (f x y z w) @@ -88,6 +91,9 @@ Ltac on_call f tac := end | |- ?T => match T with + | context [f ?x ?y ?z ?w ?v ?u ?a ?b ?c] => tac (f x y z w v u a b c) + | context [f ?x ?y ?z ?w ?v ?u ?a ?b] => tac (f x y z w v u a b) + | context [f ?x ?y ?z ?w ?v ?u ?a] => tac (f x y z w v u a) | context [f ?x ?y ?z ?w ?v ?u] => tac (f x y z w v u) | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) | context [f ?x ?y ?z ?w] => tac (f x y z w) diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index a87eda0a26..a268f0afb5 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -28,8 +28,16 @@ Notation " ! " := (False_rect _ _). (** Abbreviation for first projection and hiding of proofs of subset objects. *) +(** The scope in which programs are typed (not their types). *) + +Delimit Scope program_scope with prg. + Notation " ` t " := (proj1_sig t) (at level 10) : core_scope. -Notation "( x & ? )" := (@exist _ _ x _) : core_scope. + +Delimit Scope subset_scope with subset. + +(* In [subset_scope] to allow masking by redefinitions for particular types. *) +Notation "( x & ? )" := (@exist _ _ x _) : subset_scope. (** Coerces objects to their support before comparing them. *) @@ -64,7 +72,3 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) (* Extract Inductive sigT => "prod" [ "" ]. *) - -(** The scope in which programs are typed (not their types). *) - -Delimit Scope program_scope with prg. |