The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

Dear Kenzi,
thanks for explaining the no-confusion homomorphism     approach 
from Equations to me (I should have known).  It contrasts the
inversion/injectivity approach of Dominique in that it uses casts.
Gert


> On 13. Feb 2021, at 15:18, Kenji Maillard <chocobodralliam AT gmail.com> wrote:
> 
> Dear Gert Smolka,
> 
> I realised one minute after sending the previous mail that the ICFP'19 
> paper of Sozeau and Mangin I mentioned before also explains how to create 
> homogeneous no-confusion principles which saves you one application of UIP 
> on nat in your example:
> 
> Definition noConfusionHomK {x z} (t : K x z) : K x z -> Type :=
>   match t in K _ z return K x z -> Type with
>   | K1 _ => fun t' => match t' return Type with | K1 _ => unit | _ => False 
> end
>   | K2 _ y z a b =>
>     fun t' => match t' in K _ z' return z = z' -> Type with
>            | K1 _ => fun _ => False
>            | K2 _ y' z' a' b' =>
>              fun zz' => { yy' : y = y' &
>                              ((rew [fun y => K x y] yy' in a = a') *
>                               (rew [fun z => K y' z] zz' in rew [fun y => K 
> y z] yy' in b = b'))%type }
>            end eq_refl
>   end.
> 
> Lemma noConfusionHomK_impl {x z} (t t' : K x z) :
>   t = t' -> noConfusionHomK t t'.
> Proof.
>   intros ->; destruct t' as [|y z a b]; cbn.
>   1: easy.
>   exists eq_refl; easy.
> Qed.
> 
> 
> From Coq.Logic Require Import Eqdep_dec.
> 
> Fact K2_injective x y z a b a' b':
>   K2 x y z a b = K2 x y z a' b' -> (a,b) = (a',b').
> Proof.
>   intros h%(noConfusionHomK_impl _ _).
>   destruct h as [yy' [aa' bb']].
>   rewrite (UIP_refl_nat _ yy') in aa', bb'.
>   rewrite <- aa', <- bb'.
>   reflexivity.
> Qed.
> 
> 
> I don't see how it would be possible to get rid of the second use of UIP 
> though...
> 
> Best regards,
> Kenji Maillard
> 
> Le 13/02/2021 à 14:21, Gert Smolka a écrit :
>> I could not let loose, this stuff is addictive.
>> Luckily I found a solution before it ruined my weekend.
>> See below.
>> 
>> Anyway, I would be thankful for pointers where these
>> kinds of things are explained.
>> 
>> Enjoy your weekend,
>> Gert
>> 
>> Fact DPI_nat :
>>   forall (p: nat -> Type) n a b, existT p n a = existT p n b -> a = b.
>> Proof.
>>   (* Follows with Coq.Logic.Eqdep_dec.UIP_refl_nat *)
>> Admitted.
>> 
>> Inductive K (x: nat) : nat -> Type :=
>> | K1: K x (S x)
>> | K2: forall y z, K x y -> K y z -> K x z.
>> 
>> Fact K2_injective x y z a b a' b':
>>   K2 x z y a b = K2 x z y a' b' -> (a,b) = (a',b').
>> Proof.
>>   intros e.
>>   pose (p y z := prod (K x z) (K z y)).
>>   pose (q y := sigT (p y)).
>>   apply (DPI_nat (p y) z).
>>   apply (DPI_nat q y).
>>   pose (f:= fun c: K x y =>
>>               match c return sigT q with
>>               | K1 _ => existT q y (existT (p y) z (a,b))
>>               | K2 _ z y a b => existT q y (existT (p y) z (a,b))
>>               end).
>>   apply (f_equal f e).
>> Qed.
>> 
>> 
>>> On 13. Feb 2021, at 12:35, Gert Smolka <smolka AT ps.uni-saarland.de> wrote:
>>> 
>>> I would like to prove
>>> 
>>> Inductive K (x: nat) : nat -> Type :=
>>> | K1: K x (S x)
>>> | K2: forall y z, K x y -> K y z -> K x z.
>>> 
>>> Fact K2_injective x y z a b a' b':
>>> K2 x y z a b = K2 x y z a' b' -> (a,b) = (a',b').
>>> 
>>> by hand in a way that is similar to the proof generated     
>>> by the dependent elimination tactic of the Equations package.
>>> Does someone have a hand proof bringing across the essential ideas?
>>> 
>>> Thanks in advance,
>>> Gert
>>> 
>>> PS. I have a simple proof exploiting the "semantic” fact (K x y -> x < y),
>>> but so far I failed in finding a "regular” proof using only routine 
>>> techniques.
>>>