(* Show that the X relation of CSS always has an output *)

Module cssexistx Import misc cssrel cssexistl cssexistm ;

Goal Monotone XpredRaw ;
Intros O P OP n w o ;
Refine pair ;
Refine fst o;
intros in ;
Refine Ex3Elim ((snd o) in) ;
intros ww l m oo;
Refine Ex3In ww l m;
Refine pair ;
Refine pair ;
Refine pair ;
Refine OP ;
Refine fst (fst (fst oo));
Refine snd (fst (fst oo));
Refine snd (fst oo);
Refine snd oo;
Save Xmonotone ;

Goal Ex[w:word] X num127 w ;
Refine ExIn wZero ;
Refine Fix_contracts XpredRaw Xmonotone ;
Refine pair ;
intros ;
Refine Eq_refl ;
intros in ;
Refine not_refl_Lt num127 ;
Refine in.1 ;
Save Xexist127 ;

[ n : nat];

[ base : {i:nat} (Lt i n) -> (in128to2048 i) -> Ex[w:word] X i w ];

(* Show we can get things from pred... *)
Goal {i:nat} (Lt i (suc n)) -> (in128to2048 i) -> Ex[w:word] X (pred i) w;
intros i lt in ;
(* Case on (pred i) < = > num127 *)
Refine Trich_rec (pred i) num127 ;
(* pred i < num 127 *)
intros ll ;
Refine Lt_strong_antisym num127 i ;
Immed ;
Refine in.1 ;
(* pred i > num 127 *)
intros ltp ;
Refine base ;
Refine Lt_resp_pred ;
Refine Eq_subst ? [x:nat] Lt x (suc n) ;
Refine i ;
Refine suc_pred ;
Refine Lt_not_zero|num127 ;
Refine in.1 ;
Immed ;
intros # ;
Immed ;
Refine Lt_imp_pred_Lt ;
Refine in.2 ;
(* pred i = num127 *)
intros eq ;
Refine Eq_subst ? [x:nat] Ex ([w:word]X x w);
Refine num127 ;
Refine Eq_sym eq ;
Refine Xexist127 ;
$Save XpredExist ;

(* Deriving this from base will give the step for the induction for X *)
Goal {i:nat} (Lt i (suc n)) -> (in128to2048 i) -> Ex[w:word] X i w;
intros i lt in ;
(**** Use cases on i<127, i=127, i>127 ****)
Refine Trich_rec i num127 ;
(* i < 127 *)
intros ll ;
Refine not_Lt_Gt i num127 ;
Immed ;
Refine in.1;
(* i > 127 *)
Intros gt ;
Refine ExElim (XpredExist i lt in);
intros ww lpred ;
(* Use existance results for L and M *)
Refine ExElim (Lproof i in);
intros l ll ;
Refine ExElim (Mproof i in);
intros m mm;
Refine ExIn (Xstep l m ww) ;
Refine Fix_contracts ;
Refine Xmonotone ;
Refine pair ;
intros _ ;
Refine not_Lt_Eq num127 i ;
Refine in.1 ;
Immed ;
intros _ ;
Refine Ex3In ww l m;
Refine pair ;
Refine pair ;
Refine pair ;
Refine lpred ;
Refine ll ;
Refine mm ;
Refine Eq_refl ;
(* i = 127 *)
intros eq ;
Refine Eq_subst ? [x:nat] Ex ([w:word]X x w);
Refine num127 ;
Refine Eq_sym eq ;
Refine Xexist127 ;
Save X_ind_step;

Discharge n ;

(* The work for the existance lemma for X *)
Goal {n:nat} {i:nat} (Lt i n) -> (in128to2048 i) -> Ex[w:word] X i w;
intros n ;
Induction n ;
intros i lt ;
Refine not_n_Lt_zero ;
Immed ;
Refine X_ind_step ;
Save Xlemma ;

(* Letting n = 2048 gives the result *)
Goal Xexist ;
Intros i in ;
Refine Xlemma num2048 i ;
Refine in.2 ;
Immed ;
Save Xproof ;