k32 (Jun 15 2020 at 19:58): k32 (Jun 15 2020 at 19:58):Hello. I am struggling with dependent pattern matching in this situation (synthetic example):
Record foo := mkFoo
{ foo1 : nat;
foo2 : (fun x => match x with
| 0 => nat
| _ => bool
end) foo1
}.
Goal forall a b c d, mkFoo a b = mkFoo c d -> False.
intros.
inversion H.
subst.
assert (b = d).
Is there a tactic to prove (b = d)?
Théo Winterhalter (Jun 15 2020 at 20:13):This is probably going to be a complicated proof (b = d). You probably will have to rely on UIP (or its proof in your particular case), though it may be the case that I'm missing something. In any case, your whole lemma is wrong but I assume that is just for the sake of the example.
Jakob Botsch Nielsen (Jun 15 2020 at 20:15):With Equations and some dependent eliminations it is provable without axioms:
Derive NoConfusionHom for foo.
Goal forall a b c d, mkFoo a b = mkFoo c d -> False.
intros.
inversion H.
subst.
assert (b = d).
{ destruct c.
- now depelim H2.
- depelim H2.
cbn.
now destruct H0. }
There is probably a more straightforward way :smile:
k32 (Jun 15 2020 at 20:17):Yes, please don't mind the top goal (False). It was a bit cumbersome to write down type of b = d before subst.
Théo Winterhalter (Jun 15 2020 at 20:31):Yes, I did not mean with the UIP axiom but its proof. And here, the complicated proof is done by Derive NoConfusion.
k32 (Jun 15 2020 at 21:46):Ok, that did work for the synthetic example, but not in a general case :
Record foo {f : nat -> Type} :=
mkFoo
{ foo1 : nat;
foo2 : f foo1
}.
This time I fear it is more complicated, and maybe not provable without UIP?
Gaëtan Gilbert (Jun 15 2020 at 21:47):Jakob Botsch Nielsen said:
With Equations and some dependent eliminations it is provable without axioms:
Derive NoConfusionHom for foo. Goal forall a b c d, mkFoo a b = mkFoo c d -> False. intros. inversion H. subst. assert (b = d). { destruct c. - now depelim H2. - depelim H2. cbn. now destruct H0. }There is probably a more straightforward way :smile:
Why do you need to destruct c?
k32 (Jun 15 2020 at 21:50):...in the worst case I can make a tactic to solve this for any particular f, I guess...
Kenji Maillard (Jun 15 2020 at 22:26):Using UIP (some version can be found in Coq.Logic.Eqdep_dec) you can sort it out at least:
From Equations Require Import Equations.
From Coq Require Import Logic.Eqdep_dec.
Record foo {f : nat -> Type} :=
mkFoo
{ foo1 : nat;
foo2 : f foo1
}.
Derive NoConfusionHom for foo.
Goal forall f a (b : f a) c (d : f c), mkFoo f a b = mkFoo f c d -> True.
intros.
inversion H.
subst.
assert (b = d).
{ destruct c.
- now depelim H2.
- depelim H2.
now rewrite (UIP_refl_nat (S c) _). } (* changes the proof of S c = S c in the goal by eq_refl ultimately using the decidability of equality on nat *)
Even though tbh I think the following is more useful in general
From Equations Require Import Equations.
Record foo {f : nat -> Type} :=
mkFoo
{ foo1 : nat;
foo2 : f foo1
}.
Derive NoConfusionHom for foo.
Definition transp {A} {B : A-> Type} {x y : A} (e : x = y) : B x -> B y :=
fun bx => eq_rect x B bx y e.
Definition ap {A B} (f : A -> B) {x y : A} : x = y -> f x = f y.
Proof. now intros ->. Defined.
Goal forall f a (b : f a) c (d : f c)
(H : mkFoo f a b = mkFoo f c d),
transp (ap foo1 H) b = d.
Proof.
intros. depelim H. reflexivity.
Defined.
Thanks everyone for the input!
Cyril Cohen (Jun 16 2020 at 00:06):Note that what creates the need for UIP is the start of your script @k32 indeed, in
intros.
inversion H.
the tactic inversion does a reeeealy bad job: it generates an equality e1 : a = b on the first components as expected, but since it does not know how to deal with dependent pairs, the second components are repackaged and equated as an equality between generic Coq sigma types, inside which there is a second equality e2 : a = b, still on the first components, which is thus the one that must be used to equate the second components via a transport (as noted by @Kenji Maillard ).
However in the absence of UIP, e2 would have no reason to be the same as e1. Luckly, in your example UIP holds on nat and you do not need an axiom to show in fact e1 = e2 and move forward. BTW, @Kenji Maillard script does not start with inversion and thus should not require UIP in any way.
Here, is another axiom-free, UIP-free example using the lower level ssreflect dependent elimination tactic case: _ /:
Require Import ssreflect ssrfun.
Section example.
Context {X : Type} (* does not need to be nat *) (f : X -> Type).
Record foo := mkFoo { foo1 : X; foo2 : f foo1 }.
Lemma dual_elim (P : forall a, f a -> Prop) a (b : f a) c (d : f c) :
mkFoo a b = mkFoo c d -> P a b -> P c d.
Proof.
by rewrite -[d]/(foo2 (mkFoo c d)) -[c]/(foo1 (mkFoo c d)); case: _ /.
Qed.
End example.
It shows an equality of foos allows for the simultenaous subsitution of its components in a Curryfied predicate, which I believe was the intention of the original post (which used to proceed components by components instead of simultaneously, which was the cause of the problem).
Cyril Cohen (Jun 16 2020 at 09:04):Note also that the transport theorem is a consequence of the dependent elimination foo_eq_rect:
Require Import ssreflect ssrfun.
Section example.
Context {X : Type} (* does not need to be nat *) (f : X -> Type).
Record foo := mkFoo { foo1 : X; foo2 : f foo1 }.
Lemma foo_eq_rect
(P : forall a (b : f a) c (d : f c), mkFoo a b = mkFoo c d -> Prop)
a (b : f a) c (d : f c) (e : mkFoo a b = mkFoo c d) :
P a b a b erefl -> P a b c d e.
Proof.
pose Q ab cd := match ab, cd with mkFoo a b, mkFoo c d => P a b c d end.
by move=> Prefl; have: Q (mkFoo a b) (mkFoo c d) e by case: _ / e.
Qed.
Lemma cast_foo a (b : f a) c (d : f c) (e : mkFoo a b = mkFoo c d) :
ecast c (f c) (congr1 foo1 e) b = d.
Proof. by elim/foo_eq_rect : e. Qed.
End example.
whoa, really useful stuff here, please consider posting the different solutions in the Discourse (since our Zulip is still completely opaque to general public)
Jakob Botsch Nielsen (Jun 16 2020 at 13:07):Gaëtan Gilbert said:
Jakob Botsch Nielsen said:
With Equations and some dependent eliminations it is provable without axioms:
Derive NoConfusionHom for foo. Goal forall a b c d, mkFoo a b = mkFoo c d -> False. intros. inversion H. subst. assert (b = d). { destruct c. - now depelim H2. - depelim H2. cbn. now destruct H0. }There is probably a more straightforward way :smile:
Why do you need to
destruct c?
Otherwise it seems depelim does not manage to simplify anything, it produces just another equality between sigmas.
Anton Trunov (Jun 16 2020 at 18:24):Looks like in this case writing down a proof term explicitly might be a bit more intuitive (YMMV):
Section example.
Context {X : Type} (f : X -> Type).
Record foo := mkFoo { foo1 : X; foo2 : f foo1 }.
Definition dual_elim (P : forall a, f a -> Prop) a (b : f a) c (d : f c) :
mkFoo a b = mkFoo c d -> P a b -> P c d
:=
fun (e : mkFoo a b = mkFoo c d) =>
match
e in (_ = mkFoocd)
return match mkFoocd with
| mkFoo u v => P a b -> P u v
end
with
| eq_refl => fun pab => pab
end.
End example.
Especially, provided Coq can infer some parts of that pattern-matching above and let us write simply:
Section example.
Context {X : Type} (f : X -> Type).
Record foo := mkFoo { foo1 : X; foo2 : f foo1 }.
Definition dual_elim (P : forall a, f a -> Prop) a (b : f a) c (d : f c) :
mkFoo a b = mkFoo c d -> P a b -> P c d
:=
fun (e : mkFoo a b = mkFoo c d) =>
match e in (_ = mkFoo u v) return (P a b -> P u v) with
| eq_refl => fun pab => pab
end.
End example.
Last updated: Oct 05 2023 at 02:01 UTC