oacoq.v

Class Litn Repr : Type := {
  litn : nat -> Repr;
}.

Class Litb Repr : Type := {
  litb : bool -> Repr;
}.

Class Add Repr : Type := {
  add : Repr -> Repr -> Repr
}.

Class Ifz Repr : Type := {
  ifz : Repr -> Repr -> Repr -> Repr
}.

Class All (Repr : Type) `{Litn Repr} `{Litb Repr} `{Add Repr} `{Ifz Repr} .

Definition ex1 {A : Type} `{All A}  : A :=
  ifz (add (litn 5) (litn 7)) (litb true) (litb false) .


Inductive ty := tbool | tnat.

Definition eq_ty(t1 : ty)(t2: ty) : bool := match t1,t2 with
  | tbool, tbool => true
  | tnat, tnat => true
  | _,_ => false
end. 

Instance litntype : Litn (option ty) := {|
  litn x := Some (tnat)
|}.

Instance litbtype : Litb (option ty) := {|
  litb x := Some (tbool)
|}.

Instance addtype : Add (option ty) := {|
  add x y :=  match x,y with
   |  Some tnat, Some tnat => Some tnat
   |  _, _ => None
  end
|}.

Instance ifztype : Ifz (option ty) := {|
  ifz x y z :=  match x,y,z with
   |  Some tnat, Some t1, Some t2  => if (eq_ty t1 t2) then Some t1 else None
   |  _,_,_ => None
  end
|}.

Instance alltype : All (option ty).


Definition tyex  : option ty := ex1.

Compute tyex.

Inductive val : Type := 
  | vbool : bool -> val
  | vnat : nat -> val.

Instance litnval : Litn (option val) := {|
  litn x := Some (vnat x)
|}. 

Instance litbval : Litb (option val) := {|
  litb x := Some (vbool x)
|}. 

Instance addval : Add (option val) := {|
  add x y :=  match x,y with
   |  Some (vnat x), Some (vnat y) => Some (vnat (x + y))
   |  _, _ => None
  end
|}.

Require Import Coq.Arith.EqNat.

Instance ifzval : Ifz (option val) := {|
  ifz x y z :=  match x with
   |  Some (vnat a) =>  if (beq_nat a 0) then y else z 
   |  _ => None
  end
|}.

Instance allval : All (option val).

Definition valex  : option val := ex1.

Compute valex.

Definition typesound(t: ty)(v : val) : Prop :=
  (t = tbool -> exists b, v = vbool b) /\ (t = tnat -> exists n, v = vnat n).

Lemma litnsound : forall n v t,
  litn n = Some v -> litn n = Some t -> typesound t v.
Proof.
intros. cbn in *. inversion H. inversion H0. subst. split; intros. 
- inversion H1.
- exists n. auto.
Qed.

Lemma litbsound : forall n v t,
  litb n = Some v -> litb n = Some t -> typesound t v.
Proof.
intros. cbn in *. inversion H. inversion H0. subst. split; intros. 
- exists n. auto.
- inversion H1.
Qed.

Lemma addsound:  forall t1 t2 (t: ty) v1 v2 (v: val), 
       typesound t1 v2 -> typesound t2 v2 ->
       add (Some v1) (Some v2) = Some v -> add (Some t1) (Some t2) = Some t -> 
       typesound t v.
Proof.
intros. destruct v1; destruct v2; try inversion H1.
cbn in H1. destruct t1; destruct t2; try inversion H2.  
split; intros. inversion H3. subst. exists (n+n0). reflexivity.
Qed.


Lemma ifzsound:  forall t1 t2 t3 (t: ty) v1 v2 v3 (v: val), 
       typesound t1 v2 -> typesound t2 v2 -> typesound t3 v3 ->
       ifz (Some v1) (Some v2) (Some v3) = Some v -> ifz (Some t1) (Some t2) (Some t3) = Some t -> 
       typesound t v.
Proof.
intros. destruct t1; destruct t2; destruct t3;  try inversion H3;
destruct v1; destruct v2; destruct v3; try inversion H2
; case_eq (PeanoNat.Nat.eqb n 0); intros; rewrite H4 in H6; inversion H6; cbn; subst; auto.
Qed.