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

Module cssexistm Import misc cssrel ;

Goal Monotone MpredRaw ;
Intros O P OP n w o ;
Refine pair ;
Refine fst o;
intros in ;
Refine ExElim ((snd o) in) ;
intros ww oo;
Refine ExIn ww;
Refine pair ;
Refine OP ;
Refine fst oo;
Refine snd oo;
Save Mmonotone ;

Goal Ex[w:word] M num127 w ;
Refine ExIn M127 ;
Refine Fix_contracts MpredRaw Mmonotone ;
Refine pair ;
intros ;
Refine Eq_refl ;
intros in ;
Refine not_refl_Lt num127 ;
Refine in.1 ;
Save Mexist127 ;

[ n : nat];

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

(* Show we can get things from pred... *)
Goal {i:nat} (Lt i (suc n)) -> (in128to2048 i) -> Ex[w:word] M (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]M x w);
Refine num127 ;
Refine Eq_sym eq ;
Refine Mexist127 ;
Save MpredExist ;

(* Deriving this from base will give the step for the induction for M *)
Goal {i:nat} (Lt i (suc n)) -> (in128to2048 i) -> Ex[w:word] M 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 (MpredExist i lt in);
intros ww lpred ;
Refine ExIn (Mstep ww);
Refine Fix_contracts ;
Refine Mmonotone ;
Refine pair ;
intros _ ;
Refine not_Lt_Eq num127 i ;
Refine in.1 ;
Immed ;
intros _ ;
Refine ExIn ww;
Refine pair ;
Immed ;
Refine Eq_refl ;
(* i = 127 *)
intros eq ;
Refine Eq_subst ? [x:nat] Ex ([w:word]M x w);
Refine num127 ;
Refine Eq_sym eq ;
Refine Mexist127 ;
Save M_ind_step;

Discharge n ;

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

(* Letting n = 2048 gives the result *)
Goal Mexist ;
Intros i in ;
Refine Mlemma num2048 i ;
Refine in.2 ;
Immed ;
Save Mproof ;