The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 15.11.2012 02:51, schrieb Norman Danner:
> Hello list,
>
> I am looking for a development of the simply-typed lambda calculus 
> that I could look at, as I'm having some trouble doing this on my 
> own.  I suspect my difficulties are not deep.  What I'm looking for is 
> a development along the following lines:
>
> 1. A definition of expressions (nothing complicated; just variables,
>    natural number constants, abstraction, and application).
> 2. A definition of type (nothing complicated; just N and arrow types).
> 3. A notion of type context.
> 4. A definition of 'typed G t tau', where Pi : typed G t tau means that
>    Pi is a derivation that t has type tau under type context G (below,
>    G |- t : tau).
> 5. A notion of substitution on expressions.
> 6. A proof that if G, x : sigma |- t : tau and G |- s : sigma, then
>    G |- t[s/x] : tau.
> 7. The standard full-function-space denotational semantics using nat
>    and -> to interpret N and arrow types, where den Pi xi is the
>    denotation of (the typing of) the expression t under environment
>    xi (i.e., really a definition of
>    den {G} {t} {tau} (Pi : typed G t tau) xi).
> 8. A proof that if Pi is a derivation of G |- t[s/x] : tau obtained
>    from derivations Pi_t of G, x:sigma |- t:tau and
>    Pi_s of G |- s:sigma, then
>    den Pi xi = den Pi_t (xi[x |-> den Pi_s xi]).
>
> I can do 1-7 without much difficulty.  8 is killing me.  I assume it 
> is because I am doing something sub-optimally somewhere in 1-7.
>
> I'm sure I'm not the first person to try to do this, and I think the 
> most efficient way to solve my difficulties is to see it done right.  
> I would be grateful for pointers to solutions.  Thanks!
>
>     - Norman
Here are the first six (+reduction). I formalized confluence and 
termination using these files so I think they are sound. A lot of this 
has been done by Chad and Smolka.

What you mean by 7 I do not know. Do you mean a function from term to 
Type where [type e t N] implies [[t]] = interpret N and [type e t (T -> 
U)] implies [[t]] = (interpret T) -> interpret U ?
Kind regards, jonas
(** * Simply Typed Lambda Calculus in de Bruijn Representation *)

Set Implicit Arguments.
Require Export List Arith Omega.
Tactic Notation "inv" hyp(A)  := inversion A ; subst ; clear A.

(** helpful tactics and lemmata on decidability of comparison *)

Ltac le_gt_destruct_s a b :=
destruct (le_gt_dec a b) ; try (exfalso ; omega).

Ltac le_gt_destruct :=
repeat destruct le_gt_dec ; try (exfalso ; omega).

Ltac lt_eq_lt_destruct_s a b :=
destruct (lt_eq_lt_dec a b) as [[|]|] ; try (exfalso ; omega).


Ltac lt_eq_lt_destruct :=
repeat (destruct lt_eq_lt_dec as [[|]|]) ; try (exfalso ; omega).



(** Abstract Syntax and Typing *)

Inductive ty : Type :=
| Nat : ty                      (* nat *)
| Fun : ty -> ty -> ty.         (* function type *)

Inductive tm : Type :=
| tmR : nat -> tm               (* reference *)
| tmL : ty -> tm -> tm          (* lambda *)
| tmA : tm -> tm -> tm .        (* application *)

Definition tm_eq_dec (t s : tm) : {t=s} + {t<>s}.
decide equality ; decide equality. Qed.

(** Substitution *)

(* old shift *)
Fixpoint shift' (d k : nat) (t : tm) : tm :=
match t with
| tmR x => tmR (if le_gt_dec d x then x + k else x)
| tmL T t' => tmL T (shift' (S d) k t')
| tmA t1 t2 => tmA (shift' d k t1) (shift' d k t2)
end.

(* new shift *)
Fixpoint shift d k t : tm :=
(* removed case where d = 0 for tradeoff: structure of d must be known *)
match t with
| tmR x => tmR (if le_gt_dec d x then k + x else x) (* changed x + k to k + x 
for convertibility *)
| tmL T t' => tmL T (shift (S d) k t')
| tmA t1 t2 => tmA (shift d k t1) (shift d k t2)
end.

Lemma shift_O : forall d t, shift d 0 t = t.

fix 2 ; do 2 intro ; destruct t ; simpl.

destruct le_gt_dec ; tauto.

rewrite shift_O ; tauto. 
do 2 rewrite shift_O ; tauto.
Qed.

Lemma shift_eq : forall d k t, shift' d k t = shift d k t.

fix 3 ; do 3 intro ; destruct t ; simpl.

rewrite plus_comm. tauto.

rewrite shift_eq ; tauto.

do 2 rewrite shift_eq ; tauto.
Qed.

Fixpoint subst (d : nat) (t s : tm) : tm :=
match t with
| tmR x => match lt_eq_lt_dec d x with
             | inleft (left _) => tmR (pred x)    (* x>d, free but not least 
*)
             | inleft (right _) => shift 0 d s    (* x=d, free and least *)
             | inright _ =>  tmR x                (* x<d, bound *)
           end
| tmL T t' => tmL T (subst (S d) t' s)
| tmA t1 t2 => tmA (subst d t1 s) (subst d t2 s)
end.

Lemma shift_subst_ignore : forall s t n k l, k <= l + n -> l <= k -> subst k 
(shift l (S n) s) t = shift l n s.

induction s ; simpl ; do 6 intro.

le_gt_destruct ; lt_eq_lt_destruct ; firstorder.

f_equal. apply IHs ; firstorder.

f_equal ; [ apply IHs1 | apply IHs2 ] ; firstorder.
Qed. 

Lemma shift_distr : forall t n n' l l', l <= l' -> l' <= l + n -> shift l' n' 
(shift l n t) = shift l (n + n') t.

induction t ; [ rename n into x | | ] ; do 6 intro ; simpl.

le_gt_destruct.
    f_equal. firstorder.
    tauto.
    
rewrite IHt ; firstorder.

rewrite IHt1 ; [ rewrite IHt2 | | ] ; firstorder.
Qed.

Lemma shift_subst_comm k n l u s : shift l k (subst (l + n) u s) = subst (l + 
(k + n)) (shift l k u) s.

revert k n l. induction u ; [ rename n into x | | ] ; do 3 intro ; simpl.

le_gt_destruct ; lt_eq_lt_destruct ; simpl.
    le_gt_destruct. f_equal. rewrite (S_pred x n) ; firstorder.
    rewrite shift_distr ; [ f_equal | |  ] ; firstorder. 
    le_gt_destruct. tauto. 
    le_gt_destruct. tauto. 

f_equal. change (S (l+n)) with (S l + n). apply IHu.

f_equal.
    apply IHu1.
    apply IHu2.
Qed.

Lemma subst_distr t s u n k : subst k (subst (S (k + n)) t s) (subst n u s) = 
subst (k+n) (subst k t u) s.

revert s u n k. induction t ; [ rename n into x | | ] ; do 4 intro. 

unfold subst. 
    lt_eq_lt_destruct ; 
      fold subst.
        tauto.
        apply shift_subst_ignore ; omega.
        tauto.
        change n with (0+n). rewrite shift_subst_comm.
          f_equal. firstorder.

simpl. f_equal. change (S (k+n)) with (S k + n). apply IHt.

simpl. f_equal ; [ apply IHt1 | apply IHt2 ].
Qed.

Lemma shift_perm t l l' n n' : l <= l' -> shift l n (shift l' n' t) = shift 
(l' + n) n' (shift l n t).

revert l l' n n'. induction t ; [ rename n into x | | ] ; do 5 intro ; simpl.

le_gt_destruct ; firstorder.

f_equal. apply IHt. omega.

f_equal. 
    apply IHt1. omega.
    apply IHt2. omega.
Qed.

Lemma shift_subst_comm_subst t s l n u : l <= u -> shift l n (subst u t s) = 
subst (u + n) (shift l n t) s.

revert s l n u ; induction t ; [ rename n into x | | ] ; do 5 intro ; simpl.

lt_eq_lt_destruct ; simpl ; le_gt_destruct ; firstorder.
    apply shift_distr ; omega.

f_equal.
    apply IHt. omega.

f_equal.
    apply IHt1. omega.
    apply IHt2. omega.
Qed.

Lemma shift_subst_distr p k n u s : shift (p+k) n (subst p u s) = subst p 
(shift (S (p + k)) n u) (shift k n s).

revert p k n. induction u ; [ rename n into x | | ] ; do 3 intro.

unfold subst ; unfold shift ; fold shift ; fold subst.
lt_eq_lt_destruct ; le_gt_destruct ; simpl.
    le_gt_destruct. f_equal. rewrite (S_pred x p) ; firstorder.
    le_gt_destruct. f_equal.
    rewrite plus_comm. rewrite <- shift_perm. 
        reflexivity.
        omega.
    le_gt_destruct. tauto.

simpl. f_equal. change (S (p+k)) with (S p + k). apply IHu.

simpl. f_equal.
    apply IHu1.
    apply IHu2.
Qed.


Definition neutral t : Prop := 
match t with
  | tmR _ => True
  | tmL _ _ => False
  | tmA _ _ => True
  end.

Definition neutral_dec t : {neutral t} + {~neutral t}.
destruct t ; [ left | right | left ] ; firstorder. Qed.

Require Export STLC_Reduction.
Set Implicit Arguments.

Definition context := list ty.

Inductive typeC : context -> nat -> ty -> Prop :=
| typeCO g T : typeC (T::g) 0 T
| typeCS g k T T' : typeC g k T -> typeC (T'::g) (S k) T.

Inductive type : context -> tm -> ty -> Prop :=
| typeR g x T :
  typeC g x T ->
  type g (tmR x) T
| typeL g T t T' :
  type (T::g) t T' ->
  type g (tmL T t) (Fun T T')
| typeA g t1 t2 T1 T :
  type g t1 (Fun T1 T) ->
  type g t2 T1 ->
  type g (tmA t1 t2) T.

Definition to_type T := match T with Fun _ T' => T' | _ => T end.
Definition from_type T := match T with Fun T' _ => T' | _ => T end.


Lemma type_unique g t T1 T2 :
type g t T1 -> type g t T2 -> T1 = T2.

Proof.
intros A ; revert T2 ; induction A ; intros T2 B ; inv B.

(* R *) now induction H; inv H2 ; auto.
(* L *) now f_equal ; auto.
(* A *) apply IHA1 in H2 ; apply IHA2 in H4 ; congruence. Qed.

Lemma type_R g n T a : type g (tmR n) T -> type (a::g) (tmR (S n)) T.
firstorder. do 2 constructor. inversion H. assumption. Qed.

Lemma no_type_R : forall n g T, length g <= n -> typeC g n T -> False.
fix 5. intros n g T l typ.
destruct typ. 
    inversion l.
    apply (no_type_R _ _ _ (le_S_n _ _ l) typ).
Qed.

Lemma typing_R : forall n g T, length g > n -> typeC g n (nth n g T).
induction n.
    destruct g.
        intros T l. inversion l.

        constructor.
    
    destruct g.
        intros T l. inversion l.
        
        intros T l. constructor. apply (IHn _ _ (le_S_n _ _ l)).
Qed. 

Definition type_eq_dec : forall T T' : ty, {T=T'} + {T<>T'}.
decide equality. Qed.
 
Definition type_infer (t : tm) : forall g, { T | type g t T } + ~ exists T, 
type g t T.
induction t ; intros g.
destruct (le_gt_dec (length g) n).
    right. intros [T pT]. inversion pT. apply (no_type_R l H1).

    left. exists (nth n g Nat).   
    constructor. apply (typing_R g Nat g0).
    
destruct (IHt (t::g)) as [[T typing]|notype].
    left. exists (Fun t T). constructor. assumption.
    
    right. intros [T typing]. apply notype. inversion typing.
    exists T'. assumption. 

destruct (IHt1 g) as [[T typl]|notypl].
    destruct T. 
        right. intros [T typ]. inversion typ.
        discriminate (type_unique typl H2).
        
        destruct (IHt2 g) as [[T' typr]|notypr].
            destruct (type_eq_dec T' T1).
                left.  exists T2. rewrite e in typr. apply (typeA typl typr).
                
                right. intros [t typ]. inversion typ. apply n. rewrite 
(type_unique typr H4).
                apply (f_equal from_type (type_unique H2 typl)).
            
            right.  intros [T typ]. inversion typ. apply notypr. exists T0. 
assumption.
    
    right. intros [T typ]. inversion typ. apply notypl. exists (Fun T1 T). 
assumption.

Defined.

Corollary type_dec (t : tm) : forall g T, {type g t T} + {~ type g t T}.
intros g T. 
destruct (type_infer t g) as [[T' typ']|notyp].
    destruct (type_eq_dec T T').
        left. rewrite e. assumption.
        
        right. intros typ. apply n. apply (type_unique typ typ').
    
    right. intros typ. apply notyp. exists T. assumption.
Qed.



Lemma type_L g t T1 T2 : type g (tmL T1 t) (Fun T1 T2) -> type (T1::g) t T2.
intros typ. inversion typ. assumption. Defined.

Lemma type_A g t1 t2 T2 : type g (tmA t1 t2) T2 -> { T1 | type g t1 (Fun T1 
T2) /\ type g t2 T1 }.
intros typ. destruct (type_infer t2 g) as [[T1 typr]|bogus].
    exists T1. split.
        inversion typ. rewrite (type_unique typr H4). assumption.
        
        assumption.
    
    exfalso. apply bogus. inversion typ. exists T1. assumption.
Defined.
        

Lemma type_A1 g t1 t2 T1 T2 : type g (tmA t1 t2) T2 -> type g t2 T1 -> type g 
t1 (Fun T1 T2).
intros typ typl. inversion typ. rewrite (type_unique typl H4). assumption. 
Defined.

Lemma type_A2 g t1 t2 T1 T2 : type g (tmA t1 t2) T2 -> type g t1 (Fun T1 T2) 
-> type g t2 T1.
intros typ typr. inversion typ. 
assert (typ_e : T1 = T0) by
  apply (f_equal from_type (type_unique typr H2)).  
rewrite typ_e. assumption. Defined.

Lemma inv_type_R : forall g x T D, type g (tmR x) T -> T = nth x g D.
intros g x T D ; revert g ; induction x ; intros g typ ; 
inversion typ ; inversion H1. 

tauto.

apply (IHx g1). apply (typeR H5).

Qed.

Lemma inv_type_L : forall g T1 t T, type g (tmL T1 t) T -> {T2| type (T1::g) 
t T2 /\ T = Fun T1 T2}.
intros g T1 t T typ.
destruct (type_infer t (T1::g)) as [[T2 typt]|illtyp].
    exists T2. split.
        assumption.
        
        apply (type_unique typ). constructor ; assumption.
    
    exfalso. apply illtyp. inversion typ. eexists. apply H3. 
Qed.

Definition inv_type_A := type_A.

Lemma context_ignore_l h h' g t T :
  length h <= t ->
  length h = length h' ->
  typeC (h ++ g) t T ->
    typeC (h' ++ g) t T.

Proof.

revert h h' t g. fix 1. 
destruct h ; destruct h'.
    tauto.
    discriminate.
    discriminate.
    firstorder. rename t0 into t'. rewrite <- app_comm_cons.
      destruct t1 ; [ inversion H | ].
      constructor. 
        apply (context_ignore_l h).
        apply le_S_n. firstorder.
        firstorder.
        inversion H1 ; assumption.
Qed.

Lemma context_ignore_r h h' g t T :
  length g > t ->
  typeC (g ++ h) t T ->
    typeC (g ++ h') t T.

Proof. 

revert t. induction g ; firstorder. inversion H.
destruct t. 
    inversion H0. constructor.
    assert (H' : length g > t) by (apply gt_S_n ; firstorder).
      inversion H0. constructor. apply IHg ; assumption.
Qed.

Lemma context_ignore_l_t h h' g n T : 
  length h <= n ->
  length h = length h' ->
  type (h ++ g) (tmR n) T ->
    type (h' ++ g) (tmR n) T.

Proof.

firstorder. constructor. inversion H1. 
  apply (context_ignore_l h) ; 
    assumption.
Qed.

Lemma context_ignore_r_t h h' g n T :
  length g > n ->
  type (g ++ h) (tmR n) T ->
    type (g ++ h') (tmR n) T.

Proof.

firstorder. constructor. inversion H0. 
  apply (context_ignore_r h) ; 
    assumption.
Qed.


Lemma shift_l g a b n T : type g (shift a b (tmR n)) T -> a <= n -> type g 
(tmR (b + n)) T.
simpl ; do 2 intro ; le_gt_destruct. tauto.  Qed.

Lemma shift_r g a b n T : type g (shift a b (tmR n)) T -> a > n -> type g 
(tmR n) T.
simpl ; do 2 intro ; le_gt_destruct. tauto. Qed.


Lemma shifting g g1 g2 t T :
  type (g1 ++ g) t T ->
    type (g1 ++ g2 ++ g) (shift (length g1) (length g2) t) T.

Proof. 

revert g2 g g1 T.
induction t ; [ induction g2 | | ] ; do 4 intro.
     
(* R *)
rewrite shift_O. assumption.

destruct (le_gt_dec (length g1) n).
    (* variable in g1 *)
    rewrite <- app_comm_cons. change (a::g2++g) with ((a::nil) ++ g2 ++ g). 
rewrite app_assoc.
      apply (context_ignore_l_t (a::g1)).
        le_gt_destruct. 
          simpl. apply le_n_S. apply (le_trans _ n) ;
            firstorder.
        rewrite app_length. rewrite plus_comm. firstorder.
        assert (type ((a::g1) ++ g) (tmR (S n)) T).
            do 2 constructor. inversion H. assumption.
        pose (IHg2 _ _ _ H).
          constructor. inversion t. le_gt_destruct.
          simpl ; constructor ; assumption.

     (* variable in g2 *)
     apply (context_ignore_r_t (g2 ++ g) _ g1) ; le_gt_destruct. 
         assumption.
         apply (@shift_r _ (length g1) (length g2)) ; firstorder.
     (* L *)
     intros H. inversion H. constructor. apply (IHt g2 g (t::g1)) ; 
assumption.
     (* A *)
     intros H. inversion H. econstructor. 
         apply IHt1. apply H3.
         apply IHt2. apply H5.
Qed.



Lemma context_shift_down t g n T : type (t::g) (tmR (S n)) T -> type g (tmR 
n) T.
intros H. inversion H. inversion H2. constructor ; assumption. Qed.

Lemma shifting_down_S gl T' gr t T :
  type (gl ++ T' :: gr) (shift (length gl) 1 t) T ->
    type (gl ++ gr) t T.
revert gl T' gr T ; induction t ; intros gl T' gr T typ.
simpl in typ. le_gt_destruct.
    assert (typ' : type (T'::(gl++gr)) (tmR (S n)) T). 
        apply (context_ignore_l_t (gl ++ (T' :: nil)) (T'::gl)).
            rewrite app_length. simpl. omega.
            simpl. rewrite ! app_length. simpl. omega.
            rewrite <- app_assoc. assumption.
    apply (context_shift_down typ').
    
    apply (context_ignore_r_t (T'::gr)) ;
      assumption.
    
    inversion typ. constructor. 
    rewrite app_comm_cons. apply (IHt _ T').
    simpl. assumption.
    
    inversion typ. econstructor.
        apply (IHt1 _ T').
        apply H2.
        apply (IHt2 _ T').
        apply H4.
Qed.

Lemma shifting_down gl g gr t T : 
  type (gl ++ g ++ gr) (shift (length gl) (length g) t) T ->
    type (gl ++ gr) t T .
revert gl t T ; induction g ; intros gl t T typ. 

simpl in typ. rewrite shift_O in typ. assumption.

simpl in typ. 
    assert (type (gl ++ a::gr) (shift (length gl) 1 t) T).
        change (a::gr) with ((a::nil) ++ gr). rewrite app_assoc.
        apply IHg. rewrite <- app_assoc. rewrite app_length. rewrite <- 
shift_perm. rewrite shift_distr. 
        rewrite plus_comm. unfold app at 2. rewrite app_comm_cons. change 
(1+length g) with (length (a::g)). apply typ.
        omega. omega. omega.
   apply (shifting_down_S gl a gr _ H).

Qed.

Lemma substitution g g' T' T s t :
type (g ++ T'::g') t T ->
type g' s T' ->
type (g ++ g') (subst (length g) t s) T.

Proof. revert g T ; induction t ; intros g T A B.
(* R *) apply (shifting_down _ (T'::nil) _). simpl. lt_eq_lt_destruct ; simpl 
; le_gt_destruct.
(* g < n *) rewrite <- (S_pred _ _ l). inv A. constructor. assumption.
(* g = n *) rewrite shift_distr. 
assert (type (g ++ T' :: g') (shift 0 (length g + 1) s) T 
      = type (nil ++ (g ++ T' :: nil) ++ g') (shift (length (@nil ty)) 
(length (g ++ T' :: nil)) s) T).
    rewrite app_length. simpl. rewrite <- app_assoc. tauto.
rewrite H. apply shifting. clear H.
rewrite (inv_type_R T' A). rewrite app_nth2. rewrite <- e. rewrite 
minus_diag. tauto.
omega. omega. omega.
(* g > n *) assumption.
(* L *) inv A. constructor. exact (IHt (t::g) _ H3 B).
(* A *) inv A. econstructor ; eauto. Qed.

Corollary simple_substitution g T' T s t : type (T'::g) t T -> type g s T' -> 
type g (subst 0 t s) T.
change (type g) with (type (nil ++ g)).
change (type (T'::g)) with (type (nil ++ (T'::g))).
change 0 with (length (nil : context)).
apply substitution. 
Qed.

Lemma preservation g t t' T :
type g t T -> step t t' -> type g t' T.

Proof. intros A  B ; revert g T A.
induction B ; intros g T' A ; inv A ; eauto using type.
inv H2. eapply substitution with (g:=nil) ; eauto. Defined.

(**** Free References ****)

Inductive free : nat -> tm -> Prop :=
| freeR x : free x (tmR x)
| freeL x T t : free (S x) t -> free x (tmL T t)
| freeA x t1 t2 : free x t1 \/ free x t2 -> free x (tmA t1 t2).

Lemma type_free g t T :
type g t T -> forall x, free x t -> x < length g.

Proof. intros A ; induction A ; intros n B ; inv B.
(* R *) revert dependent x. induction g ; intros x A.  now inv A.
destruct x ; inv A ; simpl ; intuition ; omega. 
(* L *) apply IHA in H1. simpl in H1. omega. 
(* A *) intuition ; auto. Qed.

(*** !!!! Typing ***)
Lemma empty_context g t T : type g t T -> forall l, type (g++l) t T.
revert g T. induction t as [x|T1 t IH|t1 IH1 t2 IH2] ; intros g T typ l. 
    apply (context_ignore_r_t nil).
    apply (type_free typ).
    constructor.
    now rewrite app_nil_r.
    
    destruct (inv_type_L typ) as [T2 [p1 e]]. subst.
    constructor. rewrite app_comm_cons. apply IH. assumption.
    
    destruct (inv_type_A typ) as [T1 [typ1 typ2]].
    econstructor. 
        apply IH1. apply typ1.
        apply IH2. apply typ2.
Qed.(** Reduction *)

Set Implicit Arguments.
Require Export STLC_Definitions.

Definition rel (X:Type) := X -> X -> Prop.

Inductive step : rel tm :=
| stepB T t s : 
  step (tmA (tmL T t) s) (subst 0 t s) (* (T.t) s -> t[0\s] *)
| stepDL T t t' : 
  step t t' ->
  step (tmL T t) (tmL T t') (* t -> t' | (T.t) -> (T.t') *) 
| stepA1 t1 t1' t2 : 
  step t1 t1' -> 
  step (tmA t1 t2) (tmA t1' t2) (* t -> t' | t u -> t' u *)
| stepA2 t1 t2 t2' : 
  step t2 t2' -> 
  step (tmA t1 t2) (tmA t1 t2'). (* t -> t' | u t -> u t' *)

(*** reflexive transitive closure ***)

Inductive star {X: Type} (R : rel X) : rel X :=
| reflexive t : star R t t
| transitive t1 t2 t3 : 
  R t1 t2 -> 
  star R t2 t3 -> 
    star R t1 t3.

Notation "R '*'" := (star R) (at level 20).

Lemma star_sub (R : rel tm) : forall a b, R a b -> (R *) a b.
  intros a b r. econstructor.
    apply r.
    constructor.
Qed.
 
Inductive wf_star {X} (R : rel X) : nat -> rel X :=
| wf_reflexive t : wf_star R 0 t t
| wf_transitive t1 t2 t3 : forall n, 
  R t1 t2 -> 
  wf_star R n t2 t3 -> 
    wf_star R (S n) t1 t3.


Ltac star_transitive H := econstructor ; [ apply H | assumption ].

Lemma wf_eq : forall {X} (R:rel X) t1 t2, R* t1 t2 <-> exists n, wf_star R n 
t1 t2.
intros R t1 t2. split.
  intros st ; induction st.
    exists 0 ; apply wf_reflexive.
    destruct IHst as [n old]. exists (S n). star_transitive H.
  intros [n wf_st] ; induction wf_st. 
    constructor.
    star_transitive H.
Qed.

(* wf lemmas *)

Lemma wf_star_invr {X} (R : rel X) : forall a c n, wf_star R (S n) a c -> 
exists b, wf_star R n a b /\ R b c.
fix 3. intros a c n st. destruct n.
  inversion st. inversion H1. exists a. split. 
    constructor.
    rewrite H6 in H0 ; assumption.
  inversion st. destruct (wf_star_invr t2 c n H1) as [a' [wfa' pa']].
   exists a'. split. 
     star_transitive H0.
     assumption.
Qed.


Lemma wf_star_ind_right {X} (R : rel X) (P : nat -> X -> X -> Prop) : 
  (forall a, P 0 a a) -> 
  (forall a b c n, wf_star R n a b -> R b c -> P n a b -> P (S n) a c) -> 
    forall a b n, wf_star R n a b -> P n a b.
intros IHrefl IHstep a b n r. revert a b P IHrefl IHstep r.
induction n ; intros a b P IHrefl IHstep r.

inv r. apply IHrefl.

rename b into c. destruct (wf_star_invr r) as [b [wfr r']].
apply (IHstep _ _ _ _ wfr r' ).
apply IHn ; try assumption.
Qed.

Lemma wf_star_trans : forall {X} (R : rel X) nl nr a b c, wf_star R nl a b -> 
wf_star R nr b c -> wf_star R (nl+nr) a c.
(* change order for later elegance *) intros X R nl nr a b c. revert b nr a c.
induction nl ; intros b nr a c wfl wfr.
  firstorder. inversion wfl. assumption.
  firstorder. destruct (wf_star_invr wfl) as [b' [wf_st pb']].
  rewrite plus_Snm_nSm. apply (IHnl b').
    assumption.
    star_transitive pb'.
Qed.

Lemma wf_star_sub {X} (R : rel X) : forall a b, R a b -> wf_star R 1 a b.
intros a b r. 
assert (st : wf_star R 0 b b) by constructor.
star_transitive r.
Qed. 

(* star lemmas *)

Lemma star_invr {X} (R : rel X) : forall a b c, R a b -> R* b c -> exists b', 
R* a b' /\ R b' c.
intros a b c. rewrite wf_eq. intros l [n w]. 
assert (wf_star R (S n) a c) by star_transitive l.
destruct (wf_star_invr H) as [b' [w' r']].
exists b'. rewrite wf_eq. split ; [ exists n | ] ; firstorder.
Qed.

Lemma star_ind_right {X} (R : rel X) (P : X -> X -> Prop) : 
  (forall a, P a a) -> 
  (forall a b c, R* a b -> R b c -> P a b -> P a c) -> 
    forall a b, R* a b -> P a b.

intros IHbase IHstep a b. rewrite wf_eq. intros [n wfab]. 
eapply (@wf_star_ind_right _ R (fun _ => P) IHbase).
intros a' b' c' n' wfa'b'. apply IHstep. rewrite wf_eq. exists n'. assumption.
apply wfab. Qed.

Lemma star_trans {X} (R : rel X) : forall a b c, R* a b -> R* b c -> R* a c.

do 3 intro. repeat rewrite wf_eq. 

intros [nl wl] [nr wr]. exists (nl + nr). apply (wf_star_trans wl wr). Qed. 

Lemma star_sub_R {X} (R : rel X) : forall a b, R a b -> R* a b.
do 2 intro. rewrite wf_eq. exists 1. apply (wf_star_sub _ _ _ H). Qed.



(*** helpful definitions ***)

(* symmetric of R *)
Definition symmetric X R (x y : X) : Prop := R y x.

(* R1 and R2 commute : x and z go to y -> y' goes to x and z *)
Definition commutes X (R1 R2 : rel X) : Prop := forall x z y, R2 x y -> R1 y 
z -> exists y', R1 x y' /\ R2 y' z.

(* R has the diamond property *)
Definition diamond X (R : rel X) : Prop := commutes R (symmetric R).

Lemma commutativity_symmetric : forall X (R1 R2 : rel X), commutes R1 R2 -> 
commutes (symmetric R2) (symmetric R1).
intros X R1 R2 c x z y r1 r2.
destruct (c z x y) as [y' pY'] ; firstorder.
Qed.

Lemma double_symmetric X R : forall x y : X, symmetric (symmetric R) x y <-> 
R x y.
tauto. Qed.

(* not really useful, but don't forget this *)
Goal ~ forall X (R1 R2 : rel X), commutes R1 R2 -> commutes R2 R1.
intros bad_comm.
pose (R1 := (fun _ y => y) : rel Prop).
pose (R2 := (fun x _ => x) : rel Prop).
assert (commutes R1 R2).
    intros x z y _. exists True. firstorder.
destruct (bad_comm Prop R1 R2 H False False True) as [y' pY'] ;
  firstorder.
Qed.


Lemma diamond_star_propagation X (R : rel X) : diamond R -> diamond (R*).

intros dR.

assert (servant : commutes (R*) (symmetric R)).
unfold commutes. fix ind 5. intros x z y sly try. revert try sly. intros [|] 
sly. 
    exists x. firstorder. constructor.
    
    (* create x' *)
    rename t2 into z', H into sry, H0 into trz'.
    destruct (dR _ _ _ sly sry) as [x' [srx slz']].
    (* create y' *)
    destruct (ind _ _ _ slz' trz') as [y' [srx' slz]].
    exists y'. split. 
        star_transitive srx. 
        
        assumption.

cbv. fix master 4. intros x z y [|] try.

exists z. split.
    assumption.
    constructor.

rename t2 into x', H into sly, H0 into tlx'.
(* we have x', next is z' *)
destruct (servant _ _ _ sly try) as [z' [trx' slz]].
(* now the y' *)
destruct (master _ _ _ tlx' trx') as [y' [trx tlz']].
exists y'. split.
    assumption.
    
    star_transitive slz.
Qed.

Definition subst_ind R n s t t' : Prop := R (subst n t s) (subst n t' s).

Lemma type_L_unique : forall T T' t t', step (tmL T t) (tmL T' t') -> T = T'.
intros T T' t t' st. inversion st. reflexivity. Qed.


Lemma subst_induced : forall n s (t t':tm) (st : step t t'), subst_ind step n 
s t t'.
(*reduction step still possible after substition?*)

fix 5. intros n s t t' st.
  destruct st ; unfold subst_ind ; try (constructor ; apply subst_induced ; 
apply st).
  change n with (0+n). rewrite <- subst_distr. simpl. constructor.
Qed.  

Lemma wf_star_subst_sub : forall n k s t t', wf_star (subst_ind step k s) n t 
t' -> subst_ind (wf_star step n) k s t t'.

induction n ; do 4 intro ; unfold subst_ind. 

intros H ; inversion H ; constructor.
intros H ; inversion H. econstructor. apply H1. apply IHn. assumption.
Qed.

Lemma wf_star_subst_strict : ~ forall n k s t t', subst_ind (wf_star step n) 
k s t t' -> wf_star (subst_ind step k s) n t t'.

intros f.

assert (forall n, tmR (S n) <> tmR 0) by
    discriminate.
assert (forall n, subst 0 (tmR (S n)) (tmR n) = subst 0 (tmR 0) (tmR n)) by 
    tauto.
assert (n : nat) by exact 0.
pose (k := 0).
pose (s := tmR n).
pose (t := tmR (S n)).
pose (t' := tmR 0).
assert (bad : subst_ind (wf_star step k) k s t t') by constructor. 

cut (subst 0 t s = subst 0 t' s).
    intro. apply (H n).
pose (worse := f 0 0 s t t' bad).
inversion worse. tauto. Qed. 

Lemma wf_star_subst_induced : forall n k s t t', wf_star step n t t' -> 
subst_ind (wf_star step n) k s t t'.
(* this is interesting because (subst_ind (wf_star step n)) is the stronger 
set. *)
induction n ; intros k s t t' wf_b ; inversion wf_b.
  constructor. 
  pose (subst_induced k s H0). 
  unfold subst_ind. econstructor. apply subst_induced. apply H0. apply IHn. 
apply H1.
Qed.

  (* (T.t) s -> t[0\s] *)
  (* t -> t' | (T.t) -> (T.t') *)
  (* t -> t' | t u -> t' u *)
  (* t -> t' | u t -> u t' *)

(*
Lemma wf_star_stepR : term reductions on step go to step*

not needed when this was written.
*)

Lemma wf_star_stepL : forall k t t' T, wf_star step k t t' -> wf_star step k 
(tmL T t) (tmL T t').

induction k ; do 4 intro ; inversion H ; econstructor.

(* base case for free *)

econstructor. apply H1. apply IHk. assumption. 
Qed.

Lemma wf_star_stepA1 : forall k t t' u, wf_star step k t t' -> wf_star step k 
(tmA t u) (tmA t' u).

induction k ; do 4 intro ; inversion H ; econstructor.

(* base case for free *)

econstructor. apply H1. apply IHk. assumption. 
Qed.


Lemma wf_star_stepA2 : forall k t u u', wf_star step k u u' -> wf_star step k 
(tmA t u) (tmA t u').

induction k ; do 4 intro ; inversion H ; econstructor.

(* base case for free *)

econstructor 4. apply H1. apply IHk. assumption. 
Qed.

Lemma star_stepL : forall t t' T, step* t t' -> step* (tmL T t) (tmL T t').
intros t t' T. rewrite wf_eq. intros [n ws]. rewrite wf_eq. exists n. exact 
(wf_star_stepL _ ws). Qed.

Lemma star_stepA1 : forall t t' s, step* t t' -> step* (tmA t s) (tmA t' s).
intros t t' s. rewrite wf_eq. intros [n ws]. rewrite wf_eq. exists n. exact 
(wf_star_stepA1 _ ws). Qed.

Lemma star_stepA2 : forall t s s', step* s s' -> step* (tmA t s) (tmA t s').
intros t s s'. rewrite wf_eq. intros [n ws]. rewrite wf_eq. exists n. exact 
(wf_star_stepA2 _ ws). Qed.

Lemma step_shift : forall s s' l h, 
  step s s' ->
  step (shift l h s) (shift l h s').

fix 5 ; intros s s' l h st. destruct st ; simpl.

change l with (0+l). rewrite shift_subst_distr. constructor.

constructor. apply step_shift. assumption.

constructor. apply step_shift. assumption.

constructor. apply step_shift. assumption.

Qed.

Lemma wf_star_step_shift : forall s s' k l h,
  wf_star step k s s' ->
  wf_star step k (shift l h s) (shift l h s').

fix 3 ; intros s s' k l h wst ; simpl ; destruct k.

inversion wst. constructor.

inversion wst. econstructor.
    apply step_shift. apply H0.

apply wf_star_step_shift. assumption.

Qed.