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.

You can do `dependent destruction o`

, but more context would help since I can't reproduce this goal locally

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.

`eq_some`

is probably in the standard library, but I didn't bother to find it.

Last updated: Jun 25 2024 at 15:02 UTC