(* Axiomatisation of a simple language *)

(* expressions for booleans and natural numbers *)

(* expr ::= Var name sort | Tr | Fa | (Xor expr expr) 
          | Num nat | Null expr | (Opn op expr expr) *)

(* A set of names for variables *)

Implicit Arguments On.
Variable name : Set.

(* two sorts *)
Inductive sort : Set := Sbool : sort | Snat : sort.

(* A parametric set of operators for natural numbers *)
Variable op : Set.

(* The set of expression *)

Inductive expr : Set := 
     Var   : name -> sort -> expr 
   | Tr    : expr 
   | Fa    : expr 
   | Xor   : expr -> expr -> expr
   | Num   : nat  -> expr 
   | Null  : expr -> expr
   | Opn   : op -> expr -> expr -> expr.

(* Two sorts for boolean and natural Numbers expressions *)

Inductive exprcorrect : sort -> expr -> Prop 
  := corvar   : (n:name)(s:sort)(exprcorrect s (Var n s))
  |  cortr    : (exprcorrect Sbool Tr)
  |  corfa    : (exprcorrect  Sbool Fa)
  |  corxor   : (b,c:expr)(exprcorrect Sbool b)->(exprcorrect Sbool c)
               ->(exprcorrect Sbool (Xor b c))
  |  cornum   : (n:nat)(exprcorrect Snat (Num n))
  |  cornull : (e:expr)(exprcorrect Snat e)->(exprcorrect Sbool (Null e))
  |  corop    : (o:op)(e,f:expr)(exprcorrect Snat e)->(exprcorrect Snat f)
              ->(exprcorrect Snat (Opn o e f)).

Hints Resolve corvar cortr corfa corxor cornum cornull corop.

(* representation of semantical values *)
(* value := bool+nat *)

Inductive semval : Set :=
     Bool : bool -> semval
   | Nat  : nat  -> semval.

(* The semantic functions for Xor and Null, internally represented *)

Definition boolxor : bool->bool->bool 
  := [b1,b2]if b1 then if b2 then false else true else b2.

Definition iszero : nat->bool 
  := [n:nat]Cases n of O => true | (S n) => false end.

(* Each value has a sort *)
Definition sort_val 
  := [v:semval]Cases v of (Bool b)=>Sbool | (Nat n)=>Snat end.

(* (valbool v)<=> Exists b:bool.v=(Bool b) *)
Inductive valbool : semval->Prop 
  := valbool_intro : (b:bool)(valbool (Bool b)).

(* (valnat v)<=> Exists n:nat.v=(Nat n) *)
Inductive valnat : semval->Prop 
  := valnat_intro : (n:nat)(valnat (Nat n)).

Hints Resolve valbool_intro valnat_intro.

(* (compat s v) if v has sort s *)

Definition compat : sort -> semval -> Prop 
  := [s,v]Cases s of Sbool => (valbool v) | Snat => (valnat v) end.

Theorem compat_sort_val 
        : (s:sort)(v:semval)(compat s v)->s=(sort_val v).
Intros s v; Case s; Destruct 1; Trivial.
Save.

(* A schematic function for semantic of operators *)

Variable semop : op->nat->nat->nat.

(* The memory *)

Definition memory := name->sort->semval.

(* The semantic of an expression *)

Section Valexpr.

(* The Value of variables in the memory *)
Variable memstate : memory.

Hypothesis memstate_correct : (n:name)(s:sort)(compat s (memstate n s)).
Hints Resolve memstate_correct.

(* Inductive definition of the value of an expression *)

Inductive exprval : expr -> semval -> Prop :=
  valvar   : (n:name)(s:sort)(exprval (Var n s) (memstate n s))
| valtr    : (exprval Tr (Bool true))
| valfa    : (exprval Fa (Bool false))
| valxor   : (f,g:expr)(bf,bg:bool)
             (exprval f (Bool bf))->(exprval g (Bool bg))
              ->(exprval (Xor f g) (Bool (boolxor bf bg)))
| valnum   : (n:nat)(exprval (Num n) (Nat n))
| valtzero : (f:expr)(nf:nat)(exprval f (Nat nf))
              ->(exprval (Null f) (Bool (iszero nf)))
| valopn   : (o:op)(f,g:expr)(nf,ng:nat)
             (exprval f (Nat nf))->(exprval g (Nat ng))
              ->(exprval (Opn o f g) (Nat (semop o nf ng))).

Hints Resolve valvar valtr valfa valxor valnum valtzero valopn.

Theorem expr_val_cor : 
   (E:expr)(s:sort)(exprcorrect s E)->(EX v:semval | (exprval E v)).

(* A more powerful induction hypothesis, the value is compatible with 
     the sort *)

Lemma expr_val_cor_dom : 
   (E:expr)(s:sort)(exprcorrect s E)
   ->(EX v:semval | (compat s v) & (exprval E v)).
Induction 1; Intros.
(* case Var *)
Exists (memstate n s0); Auto.
(* case Tr *)
Exists (Bool true); Simpl; Auto.
(* case Fa *)
Exists (Bool false); Simpl; Auto.
(* case Xor *)
Case H1; Intro valb.
Destruct 1; Intros b0 evalb.
Case H3; Intro valc.
Destruct 1; Intros b1 evalc.
Exists (Bool (boolxor b0 b1)); Simpl; Auto.
(* case Num *)
Exists (Nat n); Simpl; Auto.
(* case Null *)
Case H1; Intro vale.
Destruct 1; Intros n evale.
Exists (Bool (iszero n)); Simpl; Auto.
(* case Opn *)
Case H1; Intro vale.
Destruct 1; Intros n evale.
Case H3; Intro valf.
Destruct 1; Intros n0 evalf.
Exists (Nat (semop o n n0)); Simpl; Auto.
Save.

(* Back to the main theorem *)

Intros E s H; Case (!expr_val_cor_dom E s); Trivial; Intros.
Exists x; Auto.
Save.