The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi Jean-Francois,

I am glad you couldn't help but send another proof :) Is 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 <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