diff options
| -rw-r--r-- | test-suite/output/FunExt.out | 9 | ||||
| -rw-r--r-- | test-suite/output/FunExt.v | 49 | ||||
| -rw-r--r-- | theories/Logic/FunctionalExtensionality.v | 164 |
3 files changed, 199 insertions, 23 deletions
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out index b97fe7a88..8fde2fcad 100644 --- a/test-suite/output/FunExt.out +++ b/test-suite/output/FunExt.out @@ -1,6 +1,6 @@ The command has indeed failed with message: Ltac call to "extensionality" failed. -Tactic failure: Not a non-dependent hypothesis. +Tactic failure: Not an extensional equality. The command has indeed failed with message: Ltac call to "extensionality" failed. Tactic failure: Not an extensional equality. @@ -9,7 +9,10 @@ Ltac call to "extensionality" failed. Tactic failure: Not an extensional equality. The command has indeed failed with message: Ltac call to "extensionality" failed. -Tactic failure: Not a non-dependent hypothesis. +Tactic failure: Not an extensional equality. The command has indeed failed with message: Ltac call to "extensionality" failed. -Tactic failure: Not an extensional equality. +Tactic failure: Already an intensional equality. +The command has indeed failed with message: +In nested Ltac calls to "extensionality" and "clearbody", last call failed. +Error: Hypothesis e depends on the body of H' diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v index b5469b70b..7658ce718 100644 --- a/test-suite/output/FunExt.v +++ b/test-suite/output/FunExt.v @@ -17,11 +17,9 @@ Fail extensionality in H. Fail extensionality in H''. Abort. -(* Test rejection of dependent equality *) +(* Test success on dependent equality *) Goal forall (p : forall x, S x = x + 1), p = p -> S = fun x => x + 1. intros p H. -Fail extensionality in p. -clear H. extensionality in p. assumption. Qed. @@ -61,7 +59,7 @@ Section test2. Goal (fun b a c => f a b c) = (fun b a c => g a b c). Proof. extensionality in H. - match type of H with (fun b a c => f a b c) = (fun b' a' c' => g a' b' c') => idtac end. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. exact H. Qed. End test2. @@ -123,7 +121,48 @@ Section test8. Goal True. Proof. extensionality in H. - match type of H with (fun (_ : True) a b c => f a b c) = (fun (_ : True) a' b' c' => g a' b' c') => idtac end. + match type of H with (fun (_ : True) => f) = (fun (_ : True) => g) => idtac end. constructor. Qed. End test8. + +Section test9. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + pose H as H'. + extensionality in H. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. + exact H'. + Qed. +End test9. + +Section test10. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : f = g). + Goal True. + Proof. + Fail extensionality in H. + constructor. + Qed. +End test10. + +Section test11. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = f a b c). + Goal True. + Proof. + pose H as H'. + pose (eq_refl : H = H') as e. + extensionality in H. + Fail extensionality in H'. + clear e. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + lazymatch type of H with f = f => idtac end. + constructor. + Qed. +End test11. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 133eba702..9551fea1a 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -56,6 +56,78 @@ Proof. apply functional_extensionality in H. destruct H. reflexivity. Defined. +(** A version of [functional_extensionality_dep] which is provably + equal to [eq_refl] on [fun _ => eq_refl] *) +Definition functional_extensionality_dep_good + {A} {B : A -> Type} + (f g : forall x : A, B x) + (H : forall x, f x = g x) + : f = g + := eq_trans (eq_sym (functional_extensionality_dep f f (fun _ => eq_refl))) + (functional_extensionality_dep f g H). + +Lemma functional_extensionality_dep_good_refl {A B} f + : @functional_extensionality_dep_good A B f f (fun _ => eq_refl) = eq_refl. +Proof. + unfold functional_extensionality_dep_good; edestruct functional_extensionality_dep; reflexivity. +Defined. + +Opaque functional_extensionality_dep_good. + +Lemma forall_sig_eq_rect + {A B} (f : forall a : A, B a) + (P : { g : _ | (forall a, f a = g a) } -> Type) + (k : P (exist (fun g => forall a, f a = g a) f (fun a => eq_refl))) + g +: P g. +Proof. + destruct g as [g1 g2]. + set (g' := fun x => (exist _ (g1 x) (g2 x))). + change g2 with (fun x => proj2_sig (g' x)). + change g1 with (fun x => proj1_sig (g' x)). + clearbody g'; clear g1 g2. + cut (forall x, (exist _ (f x) eq_refl) = g' x). + { intro H'. + apply functional_extensionality_dep_good in H'. + destruct H'. + exact k. } + { intro x. + destruct (g' x) as [g'x1 g'x2]. + destruct g'x2. + reflexivity. } +Defined. + +Definition forall_eq_rect + {A B} (f : forall a : A, B a) + (P : forall g, (forall a, f a = g a) -> Type) + (k : P f (fun a => eq_refl)) + g H + : P g H + := @forall_sig_eq_rect A B f (fun g => P (proj1_sig g) (proj2_sig g)) k (exist _ g H). + +Definition forall_eq_rect_comp {A B} f P k + : @forall_eq_rect A B f P k f (fun _ => eq_refl) = k. +Proof. + unfold forall_eq_rect, forall_sig_eq_rect; simpl. + rewrite functional_extensionality_dep_good_refl; reflexivity. +Qed. + +Definition f_equal__functional_extensionality_dep_good + {A B f g} H a + : f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H) = H a. +Proof. + apply forall_eq_rect with (H := H); clear H g. + change (eq_refl (f a)) with (f_equal (fun h => h a) (eq_refl f)). + apply f_equal, functional_extensionality_dep_good_refl. +Defined. + +Definition f_equal__functional_extensionality_dep_good__fun + {A B f g} H + : (fun a => f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H)) = H. +Proof. + apply functional_extensionality_dep_good; intro a; apply f_equal__functional_extensionality_dep_good. +Defined. + (** Apply [functional_extensionality], introducing variable x. *) Tactic Notation "extensionality" ident(x) := @@ -70,22 +142,84 @@ Tactic Notation "extensionality" ident(x) := (** Iteratively apply [functional_extensionality] on an hypothesis until finding an equality statement *) - +(* Note that you can write [Ltac extensionality_in_checker tac ::= tac tt.] to get a more informative error message. *) +Ltac extensionality_in_checker tac := + first [ tac tt | fail 1 "Anomaly: Unexpected error in extensionality tactic. Please report." ]. Tactic Notation "extensionality" "in" hyp(H) := - let rec iter_fun_ext := - lazymatch type of H with - | _ = _ => exact H - | forall x, _ => - eapply functional_extensionality_dep; intro x; - (specialize (H x) || fail "Not a non-dependent hypothesis"); iter_fun_ext - | _ => fail "Not an extensional equality" - end in - let H' := fresh "H" in - simple refine (let H' := _ in _); - [shelve| - iter_fun_ext| - clearbody H'; move H' before H; - (clear H; rename H' into H) || fail "Not a non-dependent hypothesis"]. + let rec check_is_extensional_equality H := + lazymatch type of H with + | _ = _ => constr:(Prop) + | forall a : ?A, ?T + => let Ha := fresh in + constr:(forall a : A, match H a with Ha => ltac:(let v := check_is_extensional_equality Ha in exact v) end) + end in + let assert_is_extensional_equality H := + first [ let dummy := check_is_extensional_equality H in idtac + | fail 1 "Not an extensional equality" ] in + let assert_not_intensional_equality H := + lazymatch type of H with + | _ = _ => fail "Already an intensional equality" + | _ => idtac + end in + let enforce_no_body H := + (tryif (let dummy := (eval unfold H in H) in idtac) + then clearbody H + else idtac) in + let rec extensionality_step_make_type H := + lazymatch type of H with + | forall a : ?A, ?f = ?g + => constr:({ H' | (fun a => f_equal (fun h => h a) H') = H }) + | forall a : ?A, _ + => let H' := fresh in + constr:(forall a : A, match H a with H' => ltac:(let ret := extensionality_step_make_type H' in exact ret) end) + end in + let rec eta_contract T := + lazymatch (eval cbv beta in T) with + | context T'[fun a : ?A => ?f a] + => let T'' := context T'[f] in + eta_contract T'' + | ?T => T + end in + let rec lift_sig_extensionality H := + lazymatch type of H with + | sig _ => H + | forall a : ?A, _ + => let Ha := fresh in + let ret := constr:(fun a : A => match H a with Ha => ltac:(let v := lift_sig_extensionality Ha in exact v) end) in + lazymatch type of ret with + | forall a : ?A, sig (fun b : ?B => @?f a b = @?g a b) + => eta_contract (exist (fun b : (forall a : A, B) => (fun a : A => f a (b a)) = (fun a : A => g a (b a))) + (fun a : A => proj1_sig (ret a)) + (@functional_extensionality_dep_good _ _ _ _ (fun a : A => proj2_sig (ret a)))) + end + end in + let extensionality_pre_step H H_out Heq := + let T := extensionality_step_make_type H in + let H' := fresh in + assert (H' : T) by (intros; eexists; apply f_equal__functional_extensionality_dep_good__fun); + let H''b := lift_sig_extensionality H' in + case H''b; clear H'; + intros H_out Heq in + let rec extensionality_rec H H_out Heq := + lazymatch type of H with + | forall a, _ = _ + => extensionality_pre_step H H_out Heq + | _ + => let pre_H_out' := fresh H_out in + let H_out' := fresh pre_H_out' in + extensionality_pre_step H H_out' Heq; + let Heq' := fresh Heq in + extensionality_rec H_out' H_out Heq'; + subst H_out' + end in + first [ assert_is_extensional_equality H | fail 1 "Not an extensional equality" ]; + first [ assert_not_intensional_equality H | fail 1 "Already an intensional equality" ]; + (tryif enforce_no_body H then idtac else clearbody H); + let H_out := fresh in + let Heq := fresh "Heq" in + extensionality_in_checker ltac:(fun tt => extensionality_rec H H_out Heq); + (* If we [subst H], things break if we already have another equation of the form [_ = H] *) + destruct Heq; rename H_out into H. (** Eta expansion follows from extensionality. *) |