The Coq mailing list

["Chung Kil Hur" <ckh25 AT cam.ac.uk>]

Dear coq-users,

 

In order to sell my library 'Heq' :), here I demonstrate an example.
Please apologise me if you are not interested.

 

The example is taken from Adam's book 'certified programming with dependent types'.

 

We consider a notion of heterogeneous list and an append function.
Then, try to prove the associativity of the append function.

 

================
Require Import List JMeq Eqdep.

 

Set Implicit Arguments.

 

Section fhlist.
  Variable A : Type.
  Variable P : A -> Type.

 

  Fixpoint fhlist (ls : list A) : Type :=
    match ls with
      | nil => unit
      | x :: ls' => P x * fhlist ls'
    end%type.

 

  Fixpoint fhapp (ls1 ls2 : list A)
    : fhlist ls1 -> fhlist ls2 -> fhlist (ls1 ++ ls2) :=
    match ls1 with
      | nil => fun _ hls2 => hls2
      | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
    end.
  Implicit Arguments fhapp [ls1 ls2].

 

  (** using JMeq

 

  Theorem fhapp_ass : forall ls1 ls2 ls3
    (hls1 : fhlist ls1) (hls2 : fhlist ls2) (hls3 : fhlist ls3),
    JMeq (fhapp hls1 (fhapp hls2 hls3)) (fhapp (fhapp hls1 hls2) hls3).

 

  *)

 

  (** or using eq_dep

 

  Theorem fhapp_ass : forall ls1 ls2 ls3
    (hls1 : fhlist ls1) (hls2 : fhlist ls2) (hls3 : fhlist ls3),
    eq_dep _ fhlist _ (fhapp hls1 (fhapp hls2 hls3)) _ (fhapp (fhapp hls1 hls2) hls3).

 

  *)

 

 
  (** try to prove one of the above two theorems and compare your proof with the following *)

 

  Require Import Heq.

 

  Theorem fhapp_ass' : forall ls1 ls2 ls3
    (hls1 : fhlist ls1) (hls2 : fhlist ls2) (hls3 : fhlist ls3),
    {{ fhlist # fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3 }}.

 

    induction ls1; auto.
    intros. simpl. Hrewritec (IHls1 _ _ (snd hls1) hls2 hls3). reflexivity.
  Qed.

 

End fhlist.
=================

 

If you are interested in this, Please visit the following website.

 

http://www.pps.jussieu.fr/~gil/Heq/

 

Thanks!

 

Chung-Kil Hur
Laboratoire Preuves Programmes Systemes
CNRS & Universite Paris Diderot