## Stream: Coq users

### Topic: Can't destruct or rewrite

#### 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
``````

#### Lessness (Jul 08 2021 at 10:11):

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.
``````

#### Lessness (Jul 10 2021 at 13:49):

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.
``````

#### Ali Caglayan (Jul 10 2021 at 14:01):

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.
``````

#### Ali Caglayan (Jul 10 2021 at 14:02):

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