(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basics/lists/list.ma".
include "arithmetics/nat.ma".
include "basics/bool.ma".
include "Language.ma".
include "basics/finset.ma".



(* Tools *)


lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t.
#b #T #t cases b % qed.

(* use "whd in match (if ? then ? else ?);" instead of these two *)
(* however, whd fails to rewrite in some cases *)
(* to use it on hypothesis H write "whd in match(if ? then ? else ?) in H;" *)
lemma ifthenelse_true:∀T:Type[0].∀t1,t2:T.if true then t1 else t2=t1.
#T #t1 #t2 % qed.

lemma ifthenelse_false:∀T:Type[0].∀t1,t2:T.if false then t1 else t2=t2.
#T #t1 #t2 % qed.

lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).
#b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.

lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).
#b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.

(* it does not seem to be useful at all (rewriting does not simplify) *)
lemma ifthenelse_match:∀T:Type[0].∀t1,t2:T.∀b.if b then t1 else t2=match b with [true⇒ t1|false⇒ t2].
#T #t1 #t2 * [>ifthenelse_true|>ifthenelse_false] % qed.

(* are these two really needed now? *)
lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
#b #b' cases b normalize #H destruct % qed.

lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
#b #b' cases b normalize #H destruct % qed.

(* is ex_falso in the standard libary? *)
(*lemma ex_falso_quodlibet:∀P:Prop.False→ P.
#P #F cases F qed.*)
lemma ex_falso_quodlibet:False→ ∀P:Prop.P.
#F cases F qed.

(* what about this? *)
(*lemma contradiction:∀A:Prop.∀P.P→¬P→ A.
#A #P #H #Hn @(ex_falso_quodlibet ?) @(absurd P H Hn). qed.*)

lemma contradiction:∀P.P→¬P→ (∀A:Prop.A).
#P #H #Hn #A @(ex_falso_quodlibet (absurd P H Hn)) qed.

(*
lemma not_true:∀b.(b≠true)→ (b=false).#b cases b #H try(%)
@(contradiction (true=true) (refl …) H) qed.

lemma not_false:∀b.(b≠false)→ (b=true).#b cases b #H try(%)
@(contradiction (false=false) (refl …) H) qed.
*)

lemma not_bool:∀b1,b2.(b1≠b2)→ b1=(notb b2).* * normalize #H try(%)
@(contradiction (?=?) (refl …) H) qed.

lemma neq_bool:∀b1,b2.b1=(notb b2)→(b1≠b2).* * normalize #H /2 by sym_not_eq/ qed.

lemma eqb_refl:∀T:DeqSet.∀t:T.(t==t)=true.
#T #t @(\b ?) % qed. (* inversion(t==t) #H try(%) lapply(\Pf H) #ABS @(contradiction …) [@(t=t)|@refl|@ABS] qed.*)

lemma eqb_sym:∀T:DeqSet.∀t1,t2:T.(t1==t2)=(t2==t1).
#T #t1 #t2 inversion(t1==t2) #INV [lapply(\P INV)|lapply(\Pf INV)] #H [>H >eqb_refl %
|inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?)
/2 by /|%] qed.

lemma neq_refl_false:∀T.∀t:T.(t≠t)→ ∀P:Prop.P.
#T #t #H @(contradiction (t=t) (refl …) H) qed.

lemma neqb_refl_false:∀T:DeqSet.∀t:T.(t==t)=false→ ∀P:Prop.P.
#T #t #ABS @(contradiction ((t==t)=true) (eqb_refl …) ?) @neq_bool whd in match(¬true);
assumption qed.

(* Syntax *)

definition variable ≝ DeqNat.

inductive expr: Type[0] ≝
   Var: variable → expr
 | Const: DeqNat → expr
 | Plus: expr → expr → expr
 | Minus: expr → expr → expr.

inductive condition: Type[0] ≝
   Eq: expr → expr → condition
 | Not: condition → condition.
 
  (* technical lemmas for expr_eq*)

let rec expr_eq (e1:expr) (e2:expr):bool≝
match e1 with [Var v1⇒ match e2 with [Var v2⇒ v1==v2|_⇒ false]
|Const v1⇒ match e2 with [Const v2⇒ v1==v2|_⇒ false]
|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
].

lemma expr_eq_refl:∀e:expr.expr_eq e e=true.
#e elim e [1,2: #v change with (v==v = true); @(\b ?) %
|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.

  (* the predicate expr_eq corresponds to syntactical equality on the type expr *)

lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2.
#e1 #e2 % [2:* lapply e2 -e2 elim e1
  [1,2:#n #_ change with (n==n = true) @(\b ?) %
  |3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl]
|lapply e2 -e2 elim e1
  [1,2: #v1 #e2 cases e2
    [1,6: #v2 #H >(\P H) %
    |2,5: #v2 #H normalize in H; destruct
    |3,4,7,8: #e #f normalize #ABS destruct]
  |3,4: #e #e2 #H #K #f cases f 
    [1,2,5,6: #v2 normalize #ABS destruct
    |3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2)
    #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed.




(* for the syntactical record in Language.ma *)


  (* seq_i: type of sequential instructions *)

inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i.

definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
 sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
|sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e'))| _⇒ false]
|sInc v ⇒ match s2 with [sInc v' ⇒ (v==v')| _⇒ false]
].

  (* technical lemma(s) for seq_i_eq *)

lemma seq_i_eq_refl:∀s.seq_i_eq s s=true.
#s cases s try(#v) try(#e) try %
[ whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl %
| change with (v==v = true); >(\b ?) %] qed.

lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.
#s1 #s2 % [2: * elim s1 [2,3:#v try(#e)] @seq_i_eq_refl
|lapply s2 -s2 elim s1 [2,3:#v] [#e] #s2 cases s2 [2,3,5,6,8,9:#v'] [1,3,5: #e']
[2,3,4,6,7,8: normalize #H destruct
|1: whd in ⊢ (??%? → ?); inversion (v==v') [2: normalize #_ #H destruct]
 #EQ inversion (expr_eq e e') [2: normalize #_ #H destruct] #H #_
 >(proj1 … (expr_eq_equality …) H) >(\P EQ) %
|5: #H >(\P H) %
| // ]
qed.

  (* cond_i: type of (guards of) conditional instructions,
             i.e., possible conditions of IfThenElse *)

definition cond_i:Type[0]≝condition.

let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒ 
(andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false]
|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].

  (* technical lemma(s) for cond_i *)

lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true.
#c elim c [#e #f whd in ⊢ (??%?); >expr_eq_refl >expr_eq_refl normalize %
|#c' normalize * %] qed.

lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
#c1 #c2 % [2: * // ]
lapply c2 -c2 elim c1 [ #e1 #e2 *
[ #f1 #f2 whd in ⊢ (??%? → ?);
  inversion(expr_eq e1 f1) [2: #_ normalize #EQ destruct ] #H1
  >(proj1 … (expr_eq_equality …) … H1)
  inversion(expr_eq e2 f2) [2: #_ normalize #EQ destruct ] #H2 #_
  >(proj1 … (expr_eq_equality …) … H2) %
| normalize #c #H destruct
]| #c2 #IH *
[ normalize #e1 #e2 #H destruct
| #c3 #H >(IH … H) % ]]
qed.

  (* cond_i: type of (guards of) loop instructions,
             i.e., possible conditions of While *)

definition loop_i:Type[0]≝condition.

definition loop_i_eq:loop_i → loop_i → bool ≝cond_i_eq.

lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.@cond_i_eq_equality qed.

  (* io_i: type of I/O instructions (none in the language considered) *)

definition io_i ≝ False.

definition io_i_eq ≝ λi1,i2:False. true.

lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.

  (* syntactical record *)

definition DeqExpr:DeqSet≝(mk_DeqSet expr expr_eq expr_eq_equality).

definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
[@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
|@DeqExpr
|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.

          (* | IfThenElse: condition → command → command → command*)
          (* | For: variable → expr → list command → command*)
inductive command: Type[0] ≝
   Nop: command 
 | Ass: variable → expr → command
 | Inc: variable → command
 | IfThenElse: condition → list command → list command → command
 | While: condition → list command → command
 | Call: variable → expr → function → command
 | Return: expr → command
with function: Type[0] ≝
 | Fun: variable → list command → function.

definition program ≝ list command.



(* Big step, operational semantics of expressions and conditions *)


definition environment ≝ list (variable × DeqNat).

          (* definition environment ≝ variable → nat. *)

          (* definition eq_environment: environment → environment → Prop ≝
 λenv1,env2. ∀v. env1 v = env2 v.*)
 
definition eq_environment: environment → environment → Prop ≝
 λenv1,env2.env1 = env2.

          (* definition default_env : environment ≝ λ_.0.*)

definition default_env: environment ≝ nil ?.

          (*
          definition assign: environment → variable → nat → environment ≝
          λenv,v,val,x.
            match eqb x v with
             [ true ⇒ val
             | false ⇒ env x].
          *)

let rec assign (env:environment) (v:variable) (n:DeqNat):environment ≝match env with
[nil ⇒ [mk_Prod … v n]
|cons hd tl ⇒ match hd with [(mk_Prod v' n') ⇒ match (v==v') with
  [true ⇒ cons … (mk_Prod … v n) tl
  |false ⇒ cons … hd (assign tl v n)
  ]
]].

(*
definition increment: environment →variable →environment ≝
 λenv,v,x.
  match eqb x v with
   [true ⇒ (env x)+1
   | false ⇒ env x].
*)

let rec increment (env:environment) (v:variable):environment ≝match env with
[nil ⇒ nil …
|cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with
  [true ⇒ cons … (mk_Prod … v (S n)) tl
  |false ⇒ cons … hd (increment tl v)
  ]
]].

let rec read (env:environment) (v:variable):(option DeqNat)≝match env with
[nil ⇒ None …
|cons hd tl ⇒ match hd with [(mk_Prod v' n) ⇒ match (v==v') with
  [true ⇒ Some … n
  |false ⇒ read tl v
  ]
]].

(*
lemma assign_hit: ∀env,v,val. assign env v val v = val.
 #env #v #val normalize >(eqb_n_n v) normalize %
qed.
*)

lemma assign_hit: ∀env,v,val. read (assign env v val) v = Some … val.
#env elim env
[2: * #v' #val' #env' #IH #v #val whd in match (assign ???);
inversion (v==v')
 [#INV whd in ⊢ (??%?); >(\b (refl …)) %
 |#INV whd in ⊢ (??%?); >INV whd in ⊢ (??%?); @IH ]
|#v #val whd in match (assign [ ] v val); normalize >(eqb_n_n v) %]qed.

(*

[in match t] in [H1:p ... Hn:p] [⊢ p] 

p sono come termini dove ? significa qui no, % qui si' e tutti i nomi vanno usati _
e non puoi usare costanti, costruttori, induttivi, etc.

la seconda parte del pattern individua un certo numero di posizioni chiamati RADICI;
se viene omessa la seconda parte c'e' una sola radice nella radice del termine

la prima parte del pattern cerca in ogni radice il sottotermine t e la tattica
lavora su quello

NOTA BENE: sia f una funzione ricorsiva sul primo argomento e nel goal c'e'
f (S m). Allora whd in match (f ?) identifica (f (S m)) che si riduce.
Mentre whd in match f identifica solo f che NON riduce.

 *)

(*
lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2.
 #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
qed.
*)

lemma assign_miss: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2).
 #env #v1 #v2 #val #E elim env [normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
|* #v #n #env' #IH inversion(v1==v) #INV [lapply(\P INV)|lapply(\Pf INV)] #K [destruct
whd in match (assign ???); >INV >ifthenelse_true whd in match (read (〈v,n〉::env') v2);
inversion(v2==v) #INV2 >INV2 [>ifthenelse_true|>ifthenelse_false] 
whd in match (read (〈v,val〉::env') v2); >INV2 [>ifthenelse_true|>ifthenelse_false] 
whd in match (read (〈v,n〉::env') v2); try %
lapply (\P INV2) #ABS @ex_falso_quodlibet @(absurd ? ABS E)
(*elim E #ABS2 lapply (ABS2 ABS) #F cases F*)
|whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??);
inversion(v2==v) #INV2 whd in match(if ? then ? else ?);
[whd in match (read ??); >INV2 >ifthenelse_true %
|>IH whd in match (read (〈v,n〉::env') v2);  >INV2 >ifthenelse_false %
qed.

lemma assign_miss2: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2).
 #env #v1 #v2 #val #E elim env [whd in match (assign ???); whd in match(read ??); 
 >(\bf E) >ifthenelse_false %|* #v #n #env' inversion(v==v1) #INV [<(\P INV)
 #K whd in match (assign ???); >(\b refl …) whd in match(if ? then ? else ?);
 whd in match(read (〈v,n〉::env') v2); inversion(v2==v) #INV2
 whd in match(if ? then ? else ?);  whd in match(if ? then ? else ?); whd in match(read ??);
>INV2 try(%) inversion(E) #ABS #ABS2 destruct <(\P INV) in ABS; >(\P INV2) #ABS
@(contradiction (v=v) (refl …) ?) % assumption|lapply (\Pf INV) #K whd in match (assign ???);
whd in match (read (〈v,n〉::env') v2); inversion(v2==v) #INV2 [>ifthenelse_true|>ifthenelse_false]
>(\b INV2) #H whd in match (assign ???); inversion(v1==v) #INV'
[1,3:>ifthenelse_true|2,4:>ifthenelse_false] [2,4: <H whd in match(read ??); [
>eqb_sym in INV; #INV @(contradiction ((v1==v)=true) ? ?) [@INV'|/2 by /]
|>INV2 >ifthenelse_false %]|@(contradiction ((v1==v)=true) ? ?)
[assumption|/2 by /]|whd in match (read ??); >INV2 >ifthenelse_true % qed.

let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝
 match e with
  [ Var v ⇒ read env v
  | Const n ⇒ Some ? n
  | Plus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?|Some n⇒ 
                 match sem_expr env e2 with [None ⇒ None ?|Some m⇒ Some ? (n+m)]]
  | Minus e1 e2 ⇒ match sem_expr env e1 with [None ⇒ None ?|Some n⇒ 
                 match sem_expr env e2 with [None ⇒ None ?|Some m⇒ Some ? (n-m)]]].

(*
let rec sem_condition (env:environment) (c:condition) on c : bool ≝
  match c with
   [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2)
   | Not c ⇒ notb (sem_condition env c) ].
*)

let rec sem_condition (env:environment) (c:condition) on c : option bool ≝
  match c with
   [ Eq e1 e2 ⇒ match (sem_expr env e1) with [None ⇒ None ?|Some n⇒ 
                match (sem_expr env e2) with [None ⇒ None ?|Some m⇒ Some ? (eqb n m)]]
   | Not c ⇒ match (sem_condition env c) with [None ⇒ None ?|Some b⇒ Some ? (notb b)]].



(*CERCO*)


definition imp_env_params:env_params≝mk_env_params variable.

let rec env_eq (env1:environment) (env2:environment):bool≝match env1 with
[nil ⇒ match env2 with [nil⇒ true|_ ⇒ false]
|cons hd1 tl1 ⇒ match env2 with
  [nil⇒ false
  |cons hd2 tl2 ⇒ match hd1 with
    [mk_Prod v1 n1⇒ match hd2 with
       [mk_Prod v2 n2⇒ (andb (andb (v1==v2) (n1==n2)) (env_eq tl1 tl2))]
    ]
  ]
].

lemma env_eq_refl:∀e.env_eq e e=true.
#e elim e [%|* #v #n #e' #IH normalize >(eqb_n_n v) >(eqb_n_n n) >ifthenelse_true @IH] qed.

lemma env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2.
#e1 #e2 % [2:* @env_eq_refl
|lapply e2 -e2 elim e1
  [#e2 cases e2 normalize #H try(#K #ABS) destruct %
  |* #v #n #e' #IH * normalize in match(env_eq ??);
  #p destruct cases p -p #v' #n' #e whd in match(env_eq ??); 
  inversion(v==v') #INVvv' [2: >ifthenelse_false #ABS destruct|
  inversion(n==n') #INVnn' [2: >ifthenelse_false #ABS destruct| normalize
  #EQee' >(IH e EQee') >(\P INVnn') >(\P INVvv') % qed.  

definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true.

definition store_t:Type[0]≝list (DeqEnv ×variable).

let rec store_eq (s1:store_t) (s2:store_t):bool≝
match s1 with
[nil⇒ match s2 with [nil⇒ true|_⇒ false]
|cons hd1 tl1⇒ match s2 with [nil⇒ false| cons hd2 tl2⇒ (andb (hd1==hd2) (store_eq tl1 tl2))]].

lemma store_eq_refl:∀s.store_eq s s=true.
#s elim s [%|* #e #v #tl #IH whd in match(store_eq ??); >IH
>(\b (refl …)) %
qed.

lemma store_eq_equality:∀s1,s2:store_t.store_eq s1 s2=true↔s1=s2.
#s1 #s2 % [2: * @store_eq_refl
|lapply s2 -s2 elim s1
[*
  [#_ %
  |#p #s2 normalize #ABS destruct
  ]
|#p #s2 #IH * whd in match (store_eq ??);
  [#ABS destruct
  |#p' #s whd in match (store_eq ??); inversion(p==p') #INV
    [>ifthenelse_true #H >(IH s H) >(\P INV) %
    |>ifthenelse_false #ABS destruct
    ]
  ]
] qed.

(* store is actually a stack of pairs 〈environment, return-variable〉 *)
definition imp_store:DeqSet≝mk_DeqSet store_t store_eq store_eq_equality.

definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params imp_store (*DeqEnv*).

definition current_env:store_type imp_state_params→ option environment≝λs.match s with [nil⇒ None ?
|cons hd tl⇒ match hd with [(mk_Prod env var)⇒ Some ? env]].

definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝λi,s.match i with
[sNop ⇒ Some ? s
|sAss v e ⇒ match s with
  [nil⇒ None ?
  |cons hd tl⇒ match hd with
    [(mk_Prod env var) ⇒ match (sem_expr env e) with
      [None ⇒ None ?
      | Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v n) var) tl)
      ]
    ]
  ]
|sInc v ⇒ match s with [nil⇒ None ?|cons hd tl⇒ match hd with [(mk_Prod env var)⇒ 
match (read env v) with [None ⇒ None ?|Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v (S n)) var) tl)]]]
].

definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
// qed.

definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λc,s.match c with
[Eq e1 e2⇒ match (current_env s) with
  [None ⇒ None ?
  |Some env⇒ match (sem_expr env e1) with 
    [None⇒ None ?
    |Some n ⇒ match (sem_expr env e2) with
      [None ⇒ None ?
      |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)]
    ]
  ]
|Not e ⇒ match (current_env s) with
  [None ⇒ None ?
  |Some env⇒ match (sem_condition env e) with
    [None ⇒ None ?
    |Some b ⇒ Some ? (mk_Prod ?? b s)
    ]
  ]
].

(*
let rec imp_eval_cond_cond (c: (cond_instr imp_state_params)) (s:(store_type imp_state_params)):option (bool × (store_type imp_state_params))≝
match c with
[Eq e1 e2⇒ ?
|Not c' ⇒ ?
].
*)



definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝imp_eval_cond_cond.
(*λl,s.match l with
[lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*)

definition imp_eval_call:(signature imp_state_params imp_state_params)→ expr→ imp_store→ (option imp_store)≝
λsgn,e,st.match sgn with [mk_signature fun fpt rt ⇒ match st with
  [nil ⇒ None ?
  |cons hd tl⇒ match hd with
    [mk_Prod env v ⇒ match (sem_expr env e) with
      [None ⇒ None ?
      |Some n⇒ Some ? (cons ? (mk_Prod … (assign default_env fpt n) v) st)
      ]
    ]
  ]
].

definition imp_return_call:(return_type imp_state_params)→ imp_store→ (option imp_store)≝
λr,s.match s with [nil⇒ None ?
|cons hd tl⇒ match hd with
  [mk_Prod env v ⇒ match (sem_expr env r) with
    [None ⇒ None ?
    |Some n⇒ Some ? (cons ? (mk_Prod …(assign env v n) v) tl)
    ]
  ]
].

definition imp_init_store: (store_type imp_state_params)≝(mk_Prod DeqEnv variable (nil ?) O)::(nil ?).


definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_state_params imp_eval_seq imp_eval_io
imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store.




(* Big step, declarative semantics of programs *)

definition status≝variable × (program × environment). (* indirizzo di ritorno, continuazione, ambiente *)

definition stack≝list status.

definition default_stack:stack≝nil ?.

definition push: list status → status → list status ≝
  λl,s.cons ? s l.
  
definition empty: list status → bool≝
 λl.match l with [nil ⇒ true | _ ⇒ false].

definition peek: list status → status ≝
 λl.(hd ? l (mk_Prod ? ? 0 (mk_Prod ? ? [ ] default_env))).
 
definition pop: list status → list status ≝
 λl.tail ? l.

definition Geq:expr → expr → condition≝λe1,e2.Eq (Minus e1 e2) (Const 0).

definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).

(* Abitare tipo Program *)

  (* Abitare tipo Instructions *)
  
definition imp_Instructions≝Instructions imp_state_params.

definition imp_signature≝signature imp_state_params imp_state_params.

check CallCostLabel

definition imp_envitem:(env_item imp_env_params imp_instr_params)≝

(* | mIfThenElse1:
   ∀env,st,cond,c1,c2,cont.
    sem_condition env cond = true →
    moves ((IfThenElse cond c1 c2)::cont) env st (c1::cont) env st
 | mIfThenElse2:
   ∀env,st,cond,c1,c2,cont.
    sem_condition env cond = false →
    moves ((IfThenElse cond c1 c2)::cont) env st (c2::cont) env st
*)
(* | mFor1:
    ∀env,st,v,e,l,cont.
    (sem_condition env (Lt (Var v) e))=true 
       → moves ((For v e l)::cont) env st (l@((Inc v)::(For v e l)::cont)) env st
 | mFor2:
    ∀env,st,v,e,l,cont.
    (sem_condition env (Lt (Var v) e ))=false
     → moves ((For v e l)::cont) env st cont env st
*)

inductive moves: list command → environment → stack → list command → environment → stack → Prop ≝
   mNop: ∀env,st,cont. moves (Nop::cont) env st cont env st
 | mAss: ∀env,st,v,e,cont.moves ((Ass v e)::cont) env st cont (assign env v (sem_expr env e)) st
 | mInc: ∀env,st,v,cont.moves ((Inc v)::cont) env st cont (increment env v) st
 | mIfThenElse1:
   ∀env,st,cond,l1,l2,cont.
    sem_condition env cond = true  → 
    moves ((IfThenElse cond l1 l2)::cont) env st (l1@cont) env st
 | mIfThenElse2:
   ∀env,st,cond,l1,l2,cont.
    sem_condition env cond = false → 
    moves ((IfThenElse cond l1 l2)::cont) env st (l2@cont) env st
 | mWhile1:
   ∀env,st,cond,l,cont.
     sem_condition env cond = true →
     moves ((While cond l)::cont) env st (l@(While cond l)::cont) env st
 | mWhile2:
   ∀env,st,cond,l,cont.
    sem_condition env cond = false →
    moves ((While cond l)::cont) env st cont env st
 | mCall: 
    ∀env,st,v,e,cont.∀v',l.
    moves ((Call v e (Fun v' l))::cont) env st l (assign default_env v' (sem_expr env e)) (push st (mk_Prod ? ? v (mk_Prod ? ? cont env)))
 | mReturn:
    ∀env,env',st,v,e,cont,cont'.
    moves ((Return e)::cont) env ((mk_Prod ? ? v (mk_Prod ? ? cont' env'))::st) ((Ass v e)::cont') env' st.

(* bacato: diverge silentemente nel caso lista vuota *)
inductive moves_star: list command → environment → stack → list command → environment → stack → Prop ≝
   ms_done: ∀l,env,stack. moves_star l env stack l env stack
 | ms_step: ∀l1,env1,stack1,l2,env2,stack2,l3,env3,stack3.
    moves l1 env1 stack1 l2 env2 stack2 → moves_star l2 env2 stack2 l3 env3 stack3 →
     moves_star l1 env1 stack1 l3 env3 stack3.

(* corretto anche con lista vuota di sopra *)
inductive converges: list command → environment → stack → environment → stack → Prop ≝
   conv_done: ∀l,env,stack,env',stack'.moves l env stack [ ] env' stack' → converges l env stack env' stack'
 | conv_step: ∀l,hd,tl,env,stack,env',stack',env'',stack''.moves l env stack (hd::tl) env' stack' → converges (hd::tl) env' stack' env'' stack'' →
    converges l env stack env'' stack''.

(*inductive converges: list command → environment → stack → environment → stack → Prop ≝
   conv_done: converges [] env stack env stack
 | conv_step: moves l env stack l' env' stack' → converges l' env' stack ' env'' stack'' →
    converes l env stack env'' stack''.*)


(* Examples *)

example example1:
 ∃env.
  moves_star
   [Ass 0 (Const 2)
   ;While (Not (Eq (Var 0) (Const 0)))
       [Ass 0 (Minus (Var 0) (Const 1))
       ;Ass 1 (Plus (Var 1) (Const 1))]]
   default_env
   default_stack
   (nil ?)
   env
   default_stack
   ∧ eq_environment env (assign default_env 1 2).
% [2: % [(*@(assign default_env 1 2)|%[2:normalize #v cases v [%|#v' %]|*)
@(ms_step … (mAss …)) @(ms_step …(mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …))
@(ms_step … (mWhile1 …)) [normalize %| @(ms_step …(mAss …)) @(ms_step …(mAss …)) 
@(ms_step … (mWhile2 …)) [normalize % |@(ms_done …) ]]]| normalize #v cases v normalize [%|#p cases p normalize [%|#_ %]]]] skip qed.

(* Big step, declarative semantics of diverging programs *)

(* coinductive types are greatest fixpoints generated by the constructors;
   they are built starting from the set of all terms and removing at every
   step all terms that do not start with one of the constructors listed in the
   coinductive type declaration.
   
   Intuitively, they are inhabited by all the terms of the corresponding
   inductive type and by new ``infinite'' terms obtained by chaining an infinite
   number of constructors. Intuitively again, their abstract syntax tree is
   infinite. In practice, however, we will only be able to inhabit coinductive
   types with either finite terms or with circular terms obtained by co-recursion.
   
   Recursion over coinductive types is not allowed, since the recursive functions
   could diverge on infinite (circular) term. Co-recursion is allowed to create
   circular terms *)
coinductive diverges: command → environment → Prop ≝
   cmIfThenElse1:
   ∀env,cond,c1,c2.
    sem_condition env cond = true → diverges c1 env →
    diverges (IfThenElse cond c1 c2) env
 | cmIfThenElse2:
   ∀env,cond,c1,c2.
    sem_condition env cond = false → diverges c2 env →
    diverges (IfThenElse cond c1 c2) env
 | cmIfThenElseList1:
   ∀env,cond,l1,l2.
   sem_condition env cond = true → diverges_l l1 env →
   diverges (IfThenElseList cond l1 l2) env
 | cmIfThenElseList2:
   ∀env,cond,l1,l2.
   sem_condition env cond = false → diverges_l l2 env →
   diverges (IfThenElseList cond l1 l2) env
 | cmWhile1:
   ∀env,cond,l.
    sem_condition env cond = true → diverges_l l env → diverges (While cond l) env →
    diverges (While cond l) env
 | cmWhile2:
   ∀env,env',cond,l.
    sem_condition env cond = true → moves_l l env env' → diverges (While cond l) env' →
    diverges (While cond l) env
 | cmFor:
   ∀env,v,e,l.
    ((sem_condition env (Eq (Minus e (Var v)) (Const 0))))=false → diverges_l l env → diverges (For v e l) env
with diverges_l: list command → environment → Prop ≝
   cmCons1:
    ∀env,env',he,tl.
     moves he env env' → diverges_l tl env' →
     diverges_l (he::tl) env
 | cmCons2:
    ∀env,he,tl.
     diverges he env → diverges_l (he::tl) env.

(* Examples *)

(* Here we use co-recursion to provide an infinite (circular) proof that
   the following term diverges. The env will vary at every iteration, but
   the value of the first variable will never be changed.
   
   Note: a co-recursive function (proof) must be _productive_, i.e. its weak
   head normal form must start with a constructor. I.e. in a finite number of
   steps the function must provide a first observation of the infinite term,
   where observations are identified with constructors. This is the case in
   the following definition. The exact conditions are omitted. *)
   
let corec example_div1' (x:unit) :
 ∀env. env 0 = 2 →
 diverges
    (While (Not (Eq (Var 0) (Const 0)))
       [Ass 1 (Minus (Var 0) (Const 1))
       ;Ass 1 (Plus (Var 1) (Const 1))])
  env ≝ ?.
#env #H
                          @cmWhile2 [2: normalize >H % |3:
@mCons [2:                @mAss | skip |
@mCons [3: @mNil | skip | @mAss]]| skip |
@example_div1' // @H
qed.

example example_div1:
  diverges_l
   [Ass 0 (Const 2)
   ;While (Not (Eq (Var 0) (Const 0)))
       [Ass 1 (Minus (Var 0) (Const 1))
       ;Ass 1 (Plus (Var 1) (Const 1))]]
   default_env.
@cmCons1 [2:                @mAss | skip]
@cmCons2                    @example_div1' //
qed.

(* Small step, continuation style, computational semantics of programs *)

definition status ≝ program × environment.

definition final_environment_is: status → environment → Prop ≝
 λs,env.
  match s with
  [ (*was pair*) mk_Prod l env' ⇒
    match l with
    [ nil ⇒ eq_environment env env'
    | cons _ _ ⇒ False]].

definition step: status → option status ≝
 λs.
  match s with
  [ (*was pair*) mk_Prod p env ⇒
     match p with
     [ nil ⇒ None ?
     | cons he tl ⇒
        Some …
         match he with
         [ Ass v val ⇒ 〈tl, assign env v (sem_expr env val)〉
         | Inc v ⇒ 〈tl, assign env v (sem_expr env (Plus (Var v) (Const 1)))〉
         | IfThenElse cond c1 c2 ⇒
            match sem_condition env cond with
            [ true ⇒ 〈c1::tl, env〉
            | false ⇒ 〈c2::tl, env〉]
         | IfThenElseList cond l1 l2 ⇒
            match sem_condition env cond with
            [ true ⇒ 〈l1@tl, env〉
            | false ⇒ 〈l2@tl, env〉]
         | While cond l ⇒
            match sem_condition env cond with
            [ true ⇒ 〈l@(While cond l)::tl, env〉
            | false ⇒ 〈tl, env〉]
         | For v e l ⇒
            match sem_condition env (Eq (Minus (Var v) e) (Const 0)) with
            [ true ⇒  〈tl, env〉
            | false ⇒ 〈l@(Inc v::((For v e l)::tl)), env〉
            ]            
            ]]].

let rec steps (s:status) (n:nat) on n : status ≝
 match n with
  [ O ⇒ s
  | S m ⇒
    match step s with
    [ None ⇒ s
    | Some s' ⇒ steps s' m]].

example example2:
 final_environment_is
  (steps
   〈[Ass 0 (Const 2)
    ;While (Not (Eq (Var 0) (Const 0)))
        [Ass 0 (Minus (Var 0) (Const 1))
        ;Ass 1 (Plus (Var 1) (Const 1))]]
   ,default_env〉
   20)
  (assign default_env 1 2).
 normalize 
 #v cases v normalize // #p cases p //
qed.

(* Missing from the standard library *)

lemma bool_inv_ind:
 ∀b:bool. ∀P: bool → Prop. (b=true → P true) → (b=false → P false) → P b.
 #b #P cases b /2/
qed.

lemma option_inv_ind:
 ∀A.∀x:option A. ∀P: option A → Prop.
  (x=None A → P (None A)) → (∀y. x = Some … y → P (Some … y)) → P x.
 #A #x #P cases x /2/
qed.

(* Equivalence of the two semantics on terminating programs *)

lemma moves_l_cons_invert:
 ∀hd,tl,env,env'.
  moves_l (hd::tl) env env' →
   ∃env''. moves hd env env'' ∧ moves_l tl env'' env'.
 #hd #tl #env #env'
 lapply (refl … (hd::tl)) generalize in match (hd::tl) in  ⊢ (??%? → %); #l
 #H1 #H2 cases H2 in H1;
 [ #env'' #abs destruct
 | #env1 #env2 #env'' #hd' #tl' #H1 #H2 #E destruct /3/ ]
qed.

lemma moves_l_append_invert:
 ∀l1,l2,env,env'.
  moves_l (l1@l2) env env' →
   ∃env''. moves_l l1 env env'' ∧ moves_l l2 env'' env'.
 #l1 elim l1
 [ /3/
 | #he #tl #IH #l2 #env #env' #H
   cases (moves_l_cons_invert … H)
   #env2 * #H1 #H2 cases (IH … H2) #env3 * /4/ ]
qed.

lemma commutative_plus:
∀n,m.n+m=m+n.
#n #m elim m [normalize //|#m' #IH //]qed.

lemma step_Some_to_moves_l:
 ∀l,env,p',env',env''.
  step 〈l,env〉 = Some … 〈p',env'〉 → moves_l p' env' env'' → moves_l l env env''.
 #l #env #p' #env' #env'' whd in match step; normalize nodelta cases l normalize
 [ #abs destruct
 | #he #tl normalize #E destruct -E cases he in e0; normalize nodelta
   [ #v #e #E destruct /2/
   | #v #E destruct /2/
   | #cond #c1 #c2 inversion (sem_condition env cond) normalize
     #H1 #H2 destruct
     [ #H2 cases (moves_l_cons_invert … H2) #env2 * /3/
     | #H2 cases (moves_l_cons_invert … H2) #env2 * /3/ ]
   | #cond #l1 #l2 inversion (sem_condition env cond) normalize
     #H1 #H2 destruct
     [ #H2 cases (moves_l_append_invert … H2) #env2 * /3/
     | #H2 cases (moves_l_append_invert … H2) #env2 * /3/ ]
   | #cond #l inversion (sem_condition env cond) normalize
     #H1 #H2 destruct
     [ (* entra nel while *) #H2 cases (moves_l_append_invert … H2) #env2 * #H3
       #H4 cases (moves_l_cons_invert … H4) #env3 * /3/
     | (* termina il while *) /3/ ]
     | (* caso For*) #v #e inversion(eqb(env v-sem_expr env e) 0) normalize
     #INV #l'
     [ (* sottocaso non entro nel for *)
      #HD destruct #H2 %2 [@env'|%10 normalize @INV|@H2]
      |(* sottocaso entro nel for *)
      #HD destruct #H2 cases (moves_l_append_invert … H2)
      #env2 * #H3 #H4 cases (moves_l_cons_invert … H4)
      #env3 *
      
      #H5 #H6 destruct cases (moves_l_cons_invert … H6)
      #env4 * #H7 #H8 destruct %2 [@env4|%9[3:normalize @INV|@env2|4:@H3|@env3
      |@H5|@H7]|@H8]
qed.
      
theorem steps_to_moves_l:
 ∀n,l,env,env'. steps 〈l,env〉 n = 〈[],env'〉 → moves_l l env env'.
 #n elim n
 [ #l #env #env' #H normalize in H; destruct //
 | #m #IH #l #env #env' whd in ⊢ (??%? → ?); cases l
   [ normalize #H destruct //
   | #he #tl inversion (step 〈he::tl,env〉)
     [ #abs normalize in abs; destruct
     | * #l' #env2 #H #K normalize in K; lapply (IH ??? K) /3/ ]]]
qed.

let rec moves_l_to_steps (l:?) (env:?) (env':?) (H: moves_l l env env') on H :
 ∃n1.∀n2,tl. steps 〈l@tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?
and moves_to_steps (c:?) (env:?) (env':?) (H: moves c env env') on H :
 ∃n1.∀n2,tl. steps 〈c::tl,env〉 (n1+n2) = steps 〈tl,env'〉 n2 ≝ ?.
 cases H
 [ -moves_l_to_steps -moves_to_steps #env %{0} #n2 #tl %
 | #env1 #env2 #env3 #he #tl #H1 #H2
   lapply (moves_to_steps … H1) -moves_to_steps * #n1 #K1
   lapply (moves_l_to_steps … H2) -moves_l_to_steps * #n2 #K2
   %{(n1+n2)} #n3 #tl >associative_plus >K1 @K2

 | #env1 #v #e %{1} #n #tl %
 |(* Inc *) #env1 #v %{1} #v' #tl' %
 | #env1 #env2 #cond #c1 #c2 #E
   #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
   %{(S n1)} #n2 #tl normalize >E @K
 | #env1 #env2 #cond #c1 #c2 #E
   #H lapply (moves_to_steps … H) -moves_to_steps -moves_l_to_steps * #n1 #K
   %{(S n1)} #n2 #tl normalize >E @K
 | (* IfThenElseList *) #env1 #env2 #cond #l1 #l2 #E #H1 
 lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1 
 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
 |#env1 #env2 #cond #l1 #l2 #E #H1 
 lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1 
 %{(S n1)} #n3 #tl normalize >E normalize >associative_plus >K1 %
 | #env1 #env2 #env3 #cond #l #E #H1 #H2
   lapply (moves_l_to_steps … H1) -moves_l_to_steps * #n1 #K1
   lapply (moves_to_steps … H2) -moves_to_steps * #n2 #K2
   %{(S (n1+n2))} #n3 #tl normalize >E normalize >associative_plus >K1 @K2
 | #env #cond #l #E %{1} #n #tl normalize >E %
 |(* For *) #env1 #env2 #env3 #env4 #v #e #l #E normalize in E; #HL #HMI #HMF
 lapply (moves_l_to_steps … HL) -moves_l_to_steps * #n1 #K1
  
 lapply (moves_to_steps … HMI) * #n2 #K2
 lapply (moves_to_steps … HMF) -moves_to_steps * #n3 #K3
 %{(S(n1+n2+n3))} #n #tl normalize >E normalize >associative_plus >associative_plus
>K1 >K2 >K3 % 
|#env #v #e #l #E normalize in E; %{1} #n #tl normalize >E normalize %
 ]
qed.