Require Import Arith.
Require Import Lt.
Require Import Bool.
Require Import Omega.
Require Import pseudo_term.

(* Some general facts about reduction *)
Section Reduction.
Variable R : Term -> Term -> Prop .
Variable R_lift: forall a b n m, R a  b -> R (a ↑ n # m) (b ↑ n # m ).

(* R is the base case, others are congruences case *)
Inductive Red  : Term -> Term -> Prop :=
 | Red_head : forall   b c,  R b c -> Red b c 
 | Red_red1 : forall x y z, Red x  y ->Red (x· z)  (y·z)
 | Red_red2 : forall x y z, Red x  y -> Red (z·x)  (z · y)
 | Red_lam : forall x y  , Red x  y -> Red (λ ,  x)  (λ , y)
 | Red_pi : forall x y A ,Red  x  y -> Red (Π (A), x)  (Π(A), y)
 | Red_pi2 : forall x A B, Red A  B -> Red (Π(A), x)  (Π(B), x)
.

Hint Constructors Red.
Hint Resolve R_lift.

(* the reduction have to be lift compliant *)
Lemma Red_lift: forall a b n m, Red a  b -> Red (a ↑ n # m) (b ↑ n # m ).
intros a b n m H; generalize n m; clear n m.
induction H; simpl in *; intros; eauto.
Qed.

Hint Resolve Red_lift.

(* some reductions will be "lift injective" *)
Variable R_lift_inv : forall a B n m, 
  R (a ↑ n # m) B -> exists b, B = b ↑ n # m /\ R a b.
Hint Resolve R_lift_inv.

Lemma Red_lift_inv : forall a B n m, 
  Red (a ↑ n # m) B -> exists b, B = b ↑ n # m /\ Red a b.
assert (forall A B, Red A B -> forall a n m, A =a ↑ n # m ->
  exists b, B = b ↑ n # m /\ Red a b).
induction 1; intros; subst.
destruct (R_lift_inv a c n m H) as (b& ? & ?).
exists b; intuition.
destruct a; try discriminate.
simpl in H0; destruct (le_gt_dec m v); discriminate.
injection H0; intros; subst; clear H0.
destruct (IHRed a1 n m) as (b & ? & ?); trivial.
exists (b·a2); subst; simpl; intuition. 
destruct a; try discriminate.
simpl in H0; destruct (le_gt_dec m v); discriminate.
injection H0; intros; subst; clear H0.
destruct (IHRed a2 n m) as (b & ? & ?); trivial.
exists (a1·b); subst; simpl; intuition.
destruct a; try discriminate.
simpl in H0; destruct (le_gt_dec m v); discriminate.
injection H0; intros; subst; clear H0.
destruct (IHRed a n (S m)) as (b & ? & ?); trivial.
exists (λ,b); subst; simpl; intuition.
destruct a; try discriminate.
simpl in H0; destruct (le_gt_dec m v); discriminate.
injection H0; intros; subst; clear H0.
destruct (IHRed a2 n (S m)) as (b & ? & ?); trivial.
exists (Π(a1),b); subst; simpl; intuition. 
destruct a; try discriminate.
simpl in H0; destruct (le_gt_dec m v); discriminate.
injection H0; intros; subst; clear H0.
destruct (IHRed a1 n m) as (b & ? & ?); trivial.
exists (Π(b),a2); subst; simpl; intuition.
eauto.
Qed.

Hint Resolve Red_lift_inv.

(* Reflexive & transitive closure of a reduction *)
Inductive Reds : Term -> Term -> Prop :=
 | Reds_refl : forall x, Reds x x
 | Reds_intro : forall x y, Red x y -> Reds x y
 | Reds_trans : forall x y z, Reds x y -> Reds y z -> Reds x z.

Hint Constructors Reds.

(* the R&T closure is still a congruence *)
Lemma Reds_La : forall a b , Reds a b -> Reds (λ, a) (λ, b).
intros; induction H; eauto.
Qed.

Lemma Reds_Pi : forall a b c d, Reds a b -> Reds c d -> 
  Reds (Π (a), c) (Π(b), d).
assert (forall a b c , Reds a b -> Reds (Π (a), c) (Π(b), c)).
induction 1; eauto.
assert (forall a b c , Reds a b -> Reds (Π (c), a) (Π(c), b)).
induction 1; eauto.
eauto.
Qed.

Lemma Reds_App : forall a b c d, Reds a b -> Reds c d -> 
  Reds (a· c) (b· d).
assert (forall a b c , Reds a b -> Reds (a· c) (b· c)).
induction 1; eauto.
assert (forall a b c , Reds a b -> Reds (c· a) (c· b)).
induction 1; eauto.
eauto.
Qed.

Hint Resolve Reds_App Reds_Pi Reds_La.

(* R&T closure with the size of the reduction encoded in it *)
Inductive Redsn : nat -> Term -> Term -> Prop :=
 | Redsn_refl : forall x, Redsn 0 x x
 | Redsn_intro : forall x y,  Red x y -> Redsn 1 x y
 | Redsn_trans : forall x y z n, Red x y -> Redsn n y z -> Redsn (S n) x z.

Hint Constructors Redsn.

Lemma Redsn_trans' : forall x y z n m, Redsn n x y -> Redsn m y z -> Redsn (n+m) x z.
intros x y z n m H; generalize z m; clear z m.
induction H; intros.
simpl; trivial.
change (1+m) with (S m). apply Redsn_trans with y; trivial.
change (S n+m) with (S (n+m)). apply Redsn_trans with y; trivial.
apply IHRedsn; trivial.
Qed.

Hint Resolve Redsn_trans'.

(* tool functions to put or remove the length of a reduction *)
Lemma strip_length_Reds : forall x y k, Redsn k x y -> Reds x y.
induction 1; eauto.
Qed.

Lemma set_length_Reds : forall x y, Reds x y -> exists k, Redsn k x y.
induction 1.
exists 0; intuition.
exists 1; intuition.
destruct IHReds1; destruct IHReds2.
exists (x0+x1); eauto.
Qed.

(* The marked reduction is still a congruence *)
Lemma Redsn_App : forall a b c d n m, Redsn n a c ->  Redsn m b d -> 
 Redsn (n+m) (a·b) (c·d).
assert (forall a b c n , Redsn n a c -> Redsn n (a·b) (c·b)).
induction 1; eauto.
assert (forall a b c n , Redsn n a c -> Redsn n (b·a) (b·c)).
induction 1; eauto.
eauto.
Qed.

Lemma Redsn_La : forall a b n, Redsn n a b -> Redsn n (λ, a) (λ, b).
induction 1; eauto.
Qed.

Lemma Redsn_Pi : forall a b c d n m, Redsn n a c -> Redsn m b d ->
  Redsn (n+m) (Π (a), b) (Π(c), d).
assert (forall a b c n, Redsn n a c -> Redsn n (Π (a), b) (Π(c), b)).
induction 1; eauto.
assert (forall a b c n, Redsn n a c -> Redsn n (Π (b), a) (Π(b), c)).
induction 1; eauto.
eauto.
Qed.

Hint Resolve Redsn_App Redsn_La Redsn_Pi.

(* and it behave well with the lift *)
Lemma Redsn_lift : forall a b k n m , Redsn k a b -> Redsn k (a ↑ n # m) (b ↑ n # m).
intros; induction H; eauto.
Qed.

Lemma Redsn_lift_inv : forall a b k n m, Redsn k (a ↑ n # m) b  -> 
 exists b', b = b' ↑ n # m /\ Redsn k a  b'.
assert (forall A B k, Redsn k A B -> 
 (forall a  n m, A=a ↑ n # m   ->
  exists b', B = b' ↑ n # m /\ Redsn k a b')).
induction 1; intros.
exists a; intuition.
rewrite H0 in H. apply Red_lift_inv in H. destruct H as (b' & h1 & h2).
exists b'; intuition.
rewrite H1 in H.
apply Red_lift_inv in H. destruct H as (b & h1 & h2).
destruct (IHRedsn b n0 m h1) as (b'' & h3 & h4).
exists b''; intuition.
apply Redsn_trans with b; trivial.
eauto.
Qed.

Hint Resolve Redsn_lift Redsn_lift_inv.

End Reduction.