Stream: Coq users

Topic: Can't destruct or rewrite


view this post on Zulip 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

view this post on Zulip Lessness (Jul 08 2021 at 10:11):

Solved it, kind of.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Jul 10 2021 at 14:02):

By destructing the domain hypotheses, coq is smart enough to abstract.

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC