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)
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: Oct 13 2024 at 01:02 UTC