Stream: Coq users

Topic: Destructing dependent matches

Dorian Lesbre (May 13 2023 at 09:30):

Hi, I've been medling with defining recursive function with an explicit measure via Fix,
and I've stumbled into a bit of a roadblock when trying to prove an unfolding lemma Fix _ _ F x = F x _ (Fix _ _ F).
I use std++'s lemma Fix_unfold_rel. This works fine and the goal it generates seems highly reasonable,
Here is a minimal example:

Lemma dep_match_eq {A} (f : A -> option A)
    (g h : ∀ x y, f x = Some y -> A)
    (Hgh : ∀ x y H, g x y H = h x y H) x :
  match f x as x' return f x = x' -> A with
  | Some y => fun Heq => g x y Heq
  | None => fun _ => x
  end eq_refl =
  match f x as x' return f x = x' -> A with
  | Some y => fun Heq => h x y Heq
  | None => fun _ => x
  end eq_refl.

Now I can prove this by using the functional extensionality axiom to show g = h, then rewrite and use reflexivity. However it seems like it should be provable without. Is there any way I can achieve this ? or alternatively, a better way to do this ?
(I can provide a more complete example if need be, but I think this here is the gist of my problem)

Gaëtan Gilbert (May 13 2023 at 11:09):

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.E2.9C.94.20Case.20Analysis.20with.20Dependent.20Records is related

Dorian Lesbre (May 13 2023 at 11:28):

Ok I see... It indeed the same problem (I really want to destruct (f x), but I can't.
A friend help me find a solution that work by generalizing:

Proof.
  remember (g x).
  remember (h x).
  pose (Hgh x).
  rewrite <- Heqa in e.
  rewrite <- Heqa0 in e.
  clear g h Hgh Heqa Heqa0.
  destruct (f x).
  - auto.
  - auto.
Qed.

Last updated: Apr 20 2024 at 06:02 UTC