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

#### 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: Jun 18 2024 at 10:02 UTC