Library c2pp_pre

Annexed properties for the semantics preservation of the constructor numbering

author : Zaynah Dargaye

created : 29th April 2009





Require Import List.

Require Import Coqlib.

Require Import Compare_dec.

Require Import EqNat.

Require Import Coqlib2.

Require Import AST.

Require Import Epsml.

Require Import Pml.

Require Import c2p.






Ltac monadSimpl1 :=

  match goal with

  | [ |- (bind ?F ?G = Some ?X) -> _ ] =>

      unfold bind at 1;

      generalize (refl_equal F);

      pattern F at -1 in |- *;

      case F;

      [ (let EQ := fresh "EQ" in

           (intro; intro EQ; try monadSimpl1))

      | intro; intro; discriminate ]

  | [ |- (None = Some _) -> _ ] =>

      intro; discriminate

  | [ |- (Some _ = Some _) -> _ ] =>

      let h := fresh "H" in

      (intro h; injection h; intro; clear h)

  | [ |- (_ = Some _) -> _ ] =>

      let EQ := fresh "EQ" in intro EQ

  end.




Ltac monadSimpl :=

  match goal with

  | [ |- (bind ?F ?G = Some ?X) -> _ ] => monadSimpl1

  | [ |- (None = Some _) -> _ ] => monadSimpl1

  | [ |- (Some _ = Some _) -> _ ] => monadSimpl1

  | [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1

  | [ |- (?F _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1

  | [ |- (?F _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1

  | [ |- (?F _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1

  | [ |- (?F _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1

  | [ |- (?F _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1

  end.




Ltac monadInv H :=

  generalize H; monadSimpl.

I. Sorting of pattern-matching





Inductive is_sorted : list (nat*pat)->Prop:=

| is_snil : is_sorted nil

| is_sun : forall n p , is_sorted ((n,p)::nil)

| is_scons : forall n0 n1 p0 p1 l , 

                    is_sorted ((n1,p1)::l) -> lt n0 n1 -> 

                    is_sorted ( (n0,p0)::(n1,p1)::l).




Lemma is_sorted_cons : 

 forall l a , is_sorted (a::l) -> is_sorted l /\ 

                ( forall n, (List.head l) = Some n -> lt (fst a) (fst n)).




Lemma insert_head : 

 forall l l1 n p , insert n p l = Some l1 -> 

          head l1 = Some (n,p) \/ head l1 = head l.




Lemma is_sorted_incr : 

 forall l n n0 p0 p, 

 (n0 < n)%nat -> head l = Some (n, p) -> is_sorted l -> 

 is_sorted ((n0, p0) :: l).




Lemma is_sorted_insert : 

 forall l0 l1 n p , 

  is_sorted l0 ->  insert n p l0 = Some l1 -> is_sorted l1.




Theorem is_sorted_sort : 

 forall l l1 , sort l = Some l1 -> is_sorted l1.




Theorem is_sorted_sort_eq : 

 forall l , is_sorted l -> sort l = Some l.




Lemma inf_not_in_is_sorted: 

 forall l n m , head l = Some m -> is_sorted l ->lt (fst n) (fst m) -> ~In n l.




Lemma is_sorted_norepet : 

 forall l , 

    is_sorted l -> list_norepet l.




Lemma in_is_sorted : 

 forall l a p  , is_sorted (p::l) ->In ((@fst nat pat) a) (List.map (@fst nat pat) (p::l)) ->

                   le (fst p) (fst a).




Lemma is_sorted_fst_norepet: 

 forall l , 

 is_sorted l -> list_norepet (List.map (@fst nat pat) l).







Lemma insert_not_here : 

 forall l l2 n p , is_sorted l ->insert n p l  = Some l2 -> ~In (n,p) l.




Lemma in_insert_here: 

 forall l n p l2, insert n p l = Some l2 ->

          (forall n0 p0 ,  In (n0,p0) l -> In (n0,p0) l2).




Lemma in_insert_new : 

 forall l1 l2 n p , insert n p l1 = Some l2 -> In (n,p) l2.




Lemma sort_in: 

 forall l1 l2 , sort l1 =Some l2 -> 

                  (forall n p , In (n,p) l1 -> In (n,p) l2).







Lemma sort_norepet : 

 forall l1 l2, 

  sort l1 =Some l2 -> 

  list_norepet l1 .




Lemma in_insert_inv : 

 forall l n p l2, insert n p l = Some l2 -> 

           (forall n0 p0 , In (n0,p0) l2 -> (n0,p0) = (n,p) \/ In (n0,p0) l).




Lemma in_sort_in : 

forall l1 l2, 

 sort l1 = Some l2 -> forall a : nat * pat, In a l1 <-> In a l2.




 Lemma is_sorted_inf_cons : 

 forall l a, is_sorted (a::l) -> 

  (forall b , In b l -> lt (fst a) (fst b)).




 Lemma is_sorted_bound_inf : 

 forall l a , is_sorted (a::l) -> 

 (forall k , In k (a::l) -> le (fst a) (fst k)).

II. Translation environment building and correctness





Fixpoint get_numC_list (gam : gamma) (l: list ident) {struct l}:option (list nat):= 

 match l with 

 | nil => Some nil 

 | a::m => do na <- get_num gam a ; 

                 do nm <- get_numC_list gam m ; 

                  Some (na::nm) 

 end.




Fixpoint enum_list (n p:nat) {struct n}: list nat := 

 match n with 

 | O => nil 

 | S m => (enum_list m p)++(plus m p)::nil

 end.




 Lemma enum_list_commut : 

 forall p m, enum_list (S p) m = m:: enum_list p (S m).




Lemma not_in_enum: 

 forall n m i,le (plus n m) i -> ~In i (enum_list n m).




Lemma enum_list_norepet: 

 forall n m , list_norepet (enum_list n m).




Lemma get_numC_append : 

 forall l1 l2 l3 gam , 

 get_numC_list gam (l1++l2) = Some l3 -> 

 exists l4 , exists l5, get_numC_list gam l1 = Some l4 /\ 

                               get_numC_list gam l2 = Some l5/\

                               l3 = l4++l5.




Lemma get_numC_app : 

 forall l1 l2 l3 l4 gam , 

 get_numC_list gam l1 = Some l3 -> 

 get_numC_list gam l2 = Some l4 ->

 get_numC_list gam (l1++l2) = Some (l3++l4).




Lemma enum_is_sorted : 

forall n m l, 

  List.map (@fst nat pat) l = enum_list n m -> 

  is_sorted l .




Lemma enum_sort_eq : 

 forall l n m , 

  List.map (@fst nat pat) l = enum_list n m -> 

  sort l = Some l .




Lemma  not_in_enum_inf : 

 forall n m i , 

  lt i  m -> ~In i (enum_list n m) .




Lemma nth_enum: 

 forall l n m1 m pn, 

   List.map (@fst nat pat ) l = enum_list (length l) m1 ->

   le O n -> lt n (length l) -> In ((plus n m1), Patc m pn) l -> 

   nth_error l n = Some ((plus n m1), Patc m pn).




Lemma in_enum : 

 forall n m k , le m k /\ lt k (plus n m) -> In k (enum_list n m ) .




Lemma in_enum_inv : 

 forall n m k , In k (enum_list n m ) ->le m k /\ lt k (plus n m).




Lemma enum_min : 

 forall n m k , In k (enum_list n m ) -> le  m k.




Lemma get_numC_permut : 

 forall x l l2 gam, 

 list_permut_norepet ident x l -> 

get_numC_list gam x = Some l2 ->

 list_norepet l2 -> 

 exists l0 : list nat,

    get_numC_list gam l = Some l0 /\

     list_permut_norepet nat l0 l2.







Lemma list_perm_sort : 

 forall l1 l2 ,  

 sort l1 = Some l2 -> 

 list_permut_norepet (nat*pat) l1 l2.




Lemma bound_permut_enum : 

 forall l n m , list_permut_norepet nat l (enum_list n m) -> 

 forall k , In k l <-> le m k /\ lt k (plus n m).




Lemma bound_permut_enum_inv : 

 forall l n m , 

    (forall k , In k l <-> le m k /\ lt k (plus n m)) ->

     list_norepet l ->

    list_permut_norepet nat l (enum_list n m).




Lemma enum_min_permut : 

 forall l1 l2 a  m ,  

 is_sorted (a::l1) -> 

 list_permut_norepet nat  

 (List.map (fst (A:=nat) (B:=pat)) (a::l1)) l2 ->

 (forall  k , In k l2 -> le  m k ) -> In m l2 -> 

 (fst a) = m.




Lemma list_permut_enum_sorted_eq : 

 forall l2 n m , 

 is_sorted l2 -> 

 list_permut_norepet nat  (List.map (fst (A:=nat) (B:=pat)) l2) (enum_list n m) ->

 map (fst (A:=nat) (B:=pat)) l2 = enum_list n m.







Lemma list_perm_enum_sort_enum:

forall l2 l n m , 

  list_permut_norepet nat 

   (map (fst (A:=nat) (B:=pat)) l) (enum_list n m ) -> 

 sort l = Some l2  ->

 List.map (fst (A:=nat) (B:=pat)) l2 = (enum_list n m) .