Lessness (Jul 08 2021 at 09:39): Lessness (Jul 08 2021 at 09:39):What to do in such situation? Trying to rewrite with e leads to error "Abstracting over the term "f1 x0" leads to a term ... which is ill-typed". Similar error happens when trying to destruct f1 x0.
e := H x0 H6 H4 : f1 x0 = f2 x0
______________________________________(1/1)
match f1 x0 as o return ((∃ y : R, o = Some y) → R) with
| Some b => λ _ : ∃ y : R, Some b = Some y, b
| None => λ H7 : ∃ y : R, None = Some y, apply_function_subproof H7
end H6 =
match f2 x0 as o return ((∃ y : R, o = Some y) → R) with
| Some b => λ _ : ∃ y : R, Some b = Some y, b
| None => λ H7 : ∃ y : R, None = Some y, apply_function_subproof H7
end H4
Solved it, kind of.
Ben Siraphob (Jul 10 2021 at 03:32):You can do dependent destruction o, but more context would help since I can't reproduce this goal locally
Lessness (Jul 10 2021 at 13:40):There's the context:
Definition domain {A B} (f: A -> option B) := fun x => exists y, f x = Some y.
Definition apply_function {A B} {f: A -> option B} {x} (H: domain f x): B.
Proof.
unfold domain in H. destruct (f x).
+ exact b.
+ abstract (exfalso; destruct H; congruence).
Defined.
Theorem T {A B} {f1 f2: A -> option B} (H: forall x, domain f1 x -> domain f2 x -> f1 x = f2 x):
forall x (H1: domain f1 x) (H2: domain f2 x), apply_function H1 = apply_function H2.
Proof.
intros. pose proof (H _ H1 H2). unfold apply_function.
Abort.
My solution (if it can be called that?) was to use an axiom constructive_indefinite_description from IndefiniteDescription, as I'm already using it elsewhere.
Require Import IndefiniteDescription.
Definition apply_function' {A B} {f: A -> option B} {x} (H: domain f x): B.
Proof.
unfold domain in H. apply constructive_indefinite_description in H.
destruct H. exact x0.
Defined.
Theorem T {A B} {f1 f2: A -> option B} (H: forall x, domain f1 x -> domain f2 x -> f1 x = f2 x):
forall x (H1: domain f1 x) (H2: domain f2 x), apply_function' H1 = apply_function' H2.
Proof.
intros. pose proof (H _ H1 H2). unfold apply_function'.
repeat destruct constructive_indefinite_description. congruence.
Qed.
Here is a solution:
Lemma eq_some {A} (x y : A) : Some x = Some y -> x = y.
Proof.
intro H.
inversion H.
reflexivity.
Defined.
Theorem T {A B} {f1 f2: A -> option B} (H: forall x, domain f1 x -> domain f2 x -> f1 x = f2 x):
forall x (H1: domain f1 x) (H2: domain f2 x), apply_function H1 = apply_function H2.
Proof.
intros. pose proof (H _ H1 H2). unfold apply_function.
destruct H1.
destruct H2.
rewrite e.
rewrite e0.
apply eq_some.
transitivity (f1 x).
1: apply eq_sym; assumption.
transitivity (f2 x); assumption.
Defined.
By destructing the domain hypotheses, coq is smart enough to abstract.
Ali Caglayan (Jul 10 2021 at 14:03):eq_some is probably in the standard library, but I didn't bother to find it.
Last updated: Oct 04 2023 at 23:01 UTC