The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

This one is better: 
http://www-verimag.imag.fr/~monin/Publis/itp13.pdf

Sincerely,
JF

On Thu, Feb 25, 2016 at 09:03:43AM -0300, Saulo Araujo wrote:
>    Hi Jean-Francois,
>    I am glad you couldn't help but send another proof :)
>    Is [1]http://www-verimag.imag.fr/~monin/Proof/SmallInvScalesUp/paper.pdf
>    the paper that you mentioned?
>    Sincerely,
>    Saulo
>    On Thu, Feb 25, 2016 at 8:28 AM, Jean-Francois Monin
>    
> <[2]jean-francois.monin AT imag.fr>
>  wrote:
> 
>      Hello Saul,
> 
>      I don't resist to share another short version, using a handcrafted
>      inversion technique published at ITP'13 (originally called "small
>      inversions").
> 
>      It can first be used on your previous problem for getting an element in
>      a
>      sequence implemented by a binary balanced tree.
> 
>      (*
>      
> ------------------------------------------------------------------------
>      *)
> 
>      Inductive Sequence (E:Set) : nat -> Set :=
>       | SequenceLeaf: E -> E -> Sequence E 0
>       | SequenceNode: forall n, Sequence E n -> Sequence E n -> Sequence E 
> (S
>      n).
> 
>      (* Get premises, following ITP13 paper *)
>      Definition pr_Sequence {E} {n} (s : Sequence E n) :=
>        let diag n :=
>            match n with
>              | 0 => forall X: Type, (E -> E -> X) -> X
>              | S n => forall X: Type, (Sequence E n -> Sequence E n -> X) ->
>      X
>            end in
>        match s in Sequence _ n return diag n with
>          | SequenceLeaf e0 e1 => fun X k => k e0 e1
>          | SequenceNode m s0 s1 => fun X k => k s0 s1
>        end.
> 
>      Inductive List (E:Set) : nat -> Set :=
>       | ListLeaf: E -> List E 0
>       | ListNode: forall n, E -> List E n -> List E (S n).
> 
>      Inductive Digit :=  D0 | D1.
> 
>      Fixpoint get {E : Set} {n : nat} (ds: List Digit n) : Sequence E n -> E
>      :=
>        match ds in (List _ n0) return (Sequence E n0 -> E) with
>          | ListLeaf D0 => fun t => pr_Sequence t E (fun e0 e1 => e0)
>          | ListLeaf D1 => fun t => pr_Sequence t E (fun e0 e1 => e1)
>          | ListNode x D0 l => fun t => pr_Sequence t E (fun s0 s1 => get l
>      s0)
>          | ListNode x D1 l => fun t => pr_Sequence t E (fun s0 s1 => get l
>      s1)
>         end.
> 
>      (*
>      
> ------------------------------------------------------------------------
>      *)
> 
>      Now back to testing equality on List n, we need
>      - injectivity of ListLeaf: Coq built-in injection works
>      - injectivity of ListNode: an application of pr_List similar to
>      pr_Sequence
>      - a more general version called pr_List'
> 
>      (*
>      
> ------------------------------------------------------------------------
>      *)
> 
>      (* Get premises, following ITP13 paper *)
>      Definition pr_List {E n} (s : List E n) :=
>        let diag n :=
>            match n with
>              | 0 => forall X: Type, (E -> X) -> X
>              | S n => forall X: Type, (E -> List E n -> X) -> X
>            end in
>        match s in List _ n return diag n with
>          | ListLeaf e => fun X k => k e
>          | ListNode m e s => fun X k => k e s
>        end.
> 
>      (* More general version *)
>      (* To be used when the goal depends on the destructed list *)
>      Definition pr_List' {E n} (s : List E n) :=
>        let diag n :=
>            match n return List E n -> Type with
>              | 0 => fun s => forall X: List E 0 -> Type,
>                     (forall e, X (ListLeaf E e)) -> X s
>              | S p => fun s => forall X: List E (S p) -> Type,
>                       (forall e l, X (ListNode E p e l)) -> X s
>            end in
>        match s in List _ n return diag n s with
>          | ListLeaf e => fun X k => k e
>          | ListNode m e s => fun X k => k e s
>        end.
> 
>      (* Injectivity of ListNode as an application of pr_List *)
>      Lemma inj_ListNode {E n a b u v} :
>         ListNode E n a u = ListNode E n b v ->
>         forall X: Prop, (a = b -> u = v -> X) -> X.
>      Proof.
>        intros e X.
>        change (pr_List (ListNode E n a u) _ (fun x y => (x = b -> y = v -> 
> X)
>      -> X)).
>        rewrite e; red. intro k. apply k; reflexivity.
>      Qed.
> 
>      Definition Digit_dec : forall c d: Digit, {c = d} + {c <> d}.
>      Proof.
>        destruct c; destruct d; (left; reflexivity) || (right; discriminate).
>      Defined.
> 
>      Definition list_digit_dec:
>         forall n (cs ds: List Digit n), {cs = ds} + {cs <> ds}.
>      Proof.
>      intros n cs.
>      induction cs as [c | n c cs Hcs]; intro ds; apply (pr_List' ds); clear
>      ds.
>      - intro d; destruct (Digit_dec c d) as [ e | ne ].
>        + left; congruence.
>        + right; intro e. injection e; congruence.
>      - intros d ds; destruct (Digit_dec c d) as [ e | ne ].
>        + destruct (Hcs ds) as [es | nes].
>          * left; congruence.
>          * right; intro es. apply (inj_ListNode es). congruence.
>        + right; intro es. apply (inj_ListNode es). congruence.
>      Defined.
> 
>      (*
>      
> ------------------------------------------------------------------------
>      *)
> 
>      Best,
>      Jean-Francois
> 
>      On Wed, Feb 24, 2016 at 09:00:10AM -0300, Saulo Araujo wrote:
>      >    Hi Dominique,
>      >    Thanks a lot for providing this shorter proof. I am going to study
>      it with
>      >    care so that I can apply similar techniques in other dependent 
> type
>      >    equalitity decidability proofs.
>      >    Sincerely,
>      >    Saulo
>