Initial import of SMTCoq v1.2

1 files changed, 1308 insertions, 0 deletions

diff --git a/src/SMT_terms.v b/src/SMT_terms.v
new file mode 100644
index 0000000..5f6120e
--- /dev/null
+++ b/src/SMT_terms.v
@@ -0,0 +1,1308 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2015                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - MSR-Inria Joint Lab                  *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+Add LoadPath "." as SMTCoq.
+Require Import Bool List Int63 PArray.
+Require Import Misc State.
+
+Local Open Scope array_scope.
+Local Open Scope int63_scope.
+
+Hint Unfold is_true.
+
+
+(* Remark: I use Notation instead of Definition du eliminate conversion check during the type checking *)
+Notation atom := int (only parsing).
+
+Module Form.
+
+  Notation fargs := (array _lit) (only parsing).
+
+  Inductive form : Type :=
+  | Fatom (_:atom)
+  | Ftrue
+  | Ffalse
+  | Fnot2 (_:int) (_:_lit)
+  | Fand (_:fargs)
+  | For  (_:fargs)
+  | Fimp (_:fargs)
+  | Fxor (_:_lit) (_:_lit)
+  | Fiff (_:_lit) (_:_lit)
+  | Fite (_:_lit) (_:_lit) (_:_lit).
+
+  Definition is_Ftrue h :=
+    match h with Ftrue => true | _ => false end.
+
+  Definition is_Ffalse h :=
+    match h with Ffalse => true | _ => false end.
+
+  Lemma is_Ftrue_correct : forall h, is_Ftrue h -> h = Ftrue.
+  Proof. destruct h;trivial;discriminate. Qed.
+
+  Lemma is_Ffalse_correct : forall h, is_Ffalse h -> h = Ffalse.
+  Proof. destruct h;trivial;discriminate. Qed.
+
+  Section Interp.
+    Variable interp_atom : atom -> bool.
+
+    Section Interp_form.
+
+    (* On suppose qu'on a l'interprétation des litéraux *)
+      Variable interp_var : var -> bool.
+
+      (* Interprétation d'une formule en supposant l'interprétation
+         des litéraux *)
+      (* (les litéraux font office d'index de hachage) *)
+      Definition interp_aux (h:form) : bool :=
+        match h with
+        | Fatom a => interp_atom a
+        | Ftrue => true
+        | Ffalse => false
+        | Fnot2 i l => fold (fun b => negb (negb b)) 1 i (Lit.interp interp_var l)
+        | Fand args => afold_left _ _ true andb (Lit.interp interp_var) args
+        | For args => afold_left _ _ false orb (Lit.interp interp_var) args
+        | Fimp args => afold_right _ _ true implb (Lit.interp interp_var) args
+        | Fxor a b => xorb (Lit.interp interp_var a) (Lit.interp interp_var b)
+        | Fiff a b => Bool.eqb (Lit.interp interp_var a) (Lit.interp interp_var b)
+        | Fite a b c =>
+          if Lit.interp interp_var a then Lit.interp interp_var b
+          else Lit.interp interp_var c
+        end.
+
+    End Interp_form.
+
+    Section Interp_get.
+
+      Variable t_form : PArray.array form.
+
+      Definition t_interp : PArray.array bool :=
+        PArray.foldi_left (fun i t_b hf => 
+            t_b.[i <- interp_aux (PArray.get t_b) hf])
+        (PArray.make (PArray.length t_form) true) t_form.
+
+      Fixpoint lt_form i h:=
+        match h with
+        | Fatom _ | Ftrue | Ffalse => true
+        | Fnot2 _ l => Lit.blit l < i
+        | Fand args | For args | Fimp args =>
+          PArray.forallb (fun l => Lit.blit l < i) args
+        | Fxor a b | Fiff a b => (Lit.blit a < i) && (Lit.blit b < i) 
+        | Fite a b c => (Lit.blit a < i) && (Lit.blit b < i) && (Lit.blit c < i)
+        end.
+
+      Lemma lt_form_interp_form_aux :
+        forall f1 f2 i h,
+          (forall j, j < i -> f1 j = f2 j) ->
+          lt_form i h ->
+          interp_aux f1 h = interp_aux f2 h.
+      Proof.
+        destruct h;simpl;intros;trivial;
+          try (apply afold_left_eq;unfold is_true in H0;
+            rewrite PArray.forallb_spec in H0;intros;
+              auto using Lit.interp_eq_compat).
+        f_equal;auto using Lit.interp_eq_compat.
+        apply afold_right_eq;unfold is_true in H0;
+          rewrite PArray.forallb_spec in H0;intros;
+            auto using Lit.interp_eq_compat.
+        unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0;
+          rewrite !(Lit.interp_eq_compat f1 f2);auto.
+        unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0;
+          rewrite !(Lit.interp_eq_compat f1 f2);auto.
+        unfold is_true in H0;rewrite !andb_true_iff in H0;decompose [and] H0;
+          rewrite !(Lit.interp_eq_compat f1 f2);auto.
+      Qed.
+
+      Definition wf := PArray.forallbi lt_form t_form.
+
+      Hypothesis wf_t_i : wf.
+
+      Lemma length_t_interp : length t_interp = length t_form.
+      Proof.
+        unfold t_interp;apply PArray.foldi_left_Ind with (P := fun i a => length a = length t_form).
+        intros;rewrite length_set;trivial.
+        rewrite length_make, ltb_length;trivial.
+      Qed.
+
+      Lemma default_t_interp : default t_interp = true.
+      Proof.
+        unfold t_interp;apply PArray.foldi_left_Ind with
+          (P := fun i a => default a = true).
+        intros;rewrite default_set;trivial.
+        apply default_make.
+      Qed.
+
+      Lemma t_interp_wf : forall i, i < PArray.length t_form ->
+        t_interp.[i] = interp_aux (PArray.get t_interp) (t_form.[i]).
+      Proof.
+        set (P' i t := length t = length t_form ->
+          forall j, j < i ->
+            t.[j] = interp_aux (PArray.get t) (t_form.[j])).
+        assert (P' (length t_form) t_interp).
+        unfold is_true, wf in wf_t_i;rewrite PArray.forallbi_spec in wf_t_i.
+        unfold t_interp;apply foldi_left_Ind;unfold P';intros.
+        rewrite length_set in H1.
+        destruct (Int63Properties.reflect_eqb j i).
+        rewrite e, PArray.get_set_same.
+        apply lt_form_interp_form_aux with (2:= wf_t_i i H).
+        intros;rewrite get_set_other;trivial.
+        intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial.
+        rewrite H1;trivial.
+        assert (j < i).
+        assert ([|j|] <> [|i|]) by (intros Heq1;elim n;apply to_Z_inj;trivial).
+        generalize H2;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H);
+          auto with zarith.
+        rewrite get_set_other, H0;auto.
+        apply lt_form_interp_form_aux with
+          (2:= wf_t_i j (ltb_trans _ _ _ H3 H)).
+        intros;rewrite get_set_other;trivial.
+        intros Heq;elim (not_ltb_refl i);apply ltb_trans with j;
+          [ rewrite Heq| ];trivial.
+        elim (ltb_0 _ H0).
+        apply H;apply length_t_interp.
+      Qed.
+
+    End Interp_get.
+
+    Definition interp_state_var t_form :=
+      let t_interp := t_interp t_form in
+      PArray.get t_interp.
+
+    Register interp_aux as PrimInline.
+    Definition interp t_form := interp_aux (interp_state_var t_form).
+
+    Lemma wf_interp_form_lt :
+      forall t_form, wf t_form ->
+        forall x, x < PArray.length t_form ->
+          interp_state_var t_form x = interp t_form (t_form.[x]).
+    Proof.
+      unfold interp_state_var;intros.
+      apply t_interp_wf;trivial.
+    Qed.
+
+    Lemma wf_interp_form :
+      forall t_form, PArray.default t_form = Ftrue -> wf t_form ->
+        forall x, interp_state_var t_form x = interp t_form (t_form.[x]).
+    Proof.
+      intros t Hd Hwf x;case_eq (x < PArray.length t);intros.
+      apply wf_interp_form_lt;trivial.
+      unfold interp_state_var;rewrite !PArray.get_outofbound;trivial.
+      rewrite default_t_interp, Hd;trivial.
+      rewrite length_t_interp;trivial.
+    Qed.
+
+    Definition check_form t_form :=
+      is_Ftrue (PArray.default t_form) &&
+      is_Ftrue (t_form.[0]) &&
+      is_Ffalse (t_form.[1]) &&
+      wf t_form.
+
+    Lemma check_form_correct : forall t_form,
+       check_form t_form ->
+       ((PArray.default t_form = Ftrue /\ wf t_form) /\
+        Valuation.wf (interp_state_var t_form)).
+    Proof.
+     unfold is_true, check_form;intros t;rewrite !andb_true_iff.
+     intros H;decompose [and] H;clear H;
+     assert (PArray.default t = Ftrue) by (apply is_Ftrue_correct;trivial).
+     repeat split;trivial.
+     rewrite wf_interp_form;trivial.
+     apply is_Ftrue_correct in H4;trivial;rewrite H4;reflexivity.
+     rewrite wf_interp_form;trivial.
+     apply is_Ffalse_correct in H3;trivial;rewrite H3;discriminate.
+    Qed.
+
+  End Interp.
+
+End Form.
+
+(* TODO Move this *)
+Record typ_eqb : Type := Typ_eqb {
+  te_carrier : Type;
+  te_eqb : te_carrier -> te_carrier -> bool;
+  te_reflect : forall x y, reflect (x = y) (te_eqb x y)
+}.
+
+(* Common used types into which we interpret *)
+
+(* Unit *)
+
+Section Unit_typ_eqb.
+
+  Let carrier : Type := unit.
+
+  Let eqb : carrier -> carrier -> bool :=
+    fun _ _ => true.
+
+  Lemma unit_reflect :
+    forall x y, reflect (x = y) (eqb x y).
+  Proof.
+    unfold eqb; intros x y; case x; case y; simpl;
+      constructor; reflexivity.
+  Qed.
+
+  Definition unit_typ_eqb :=
+    Typ_eqb carrier eqb unit_reflect.
+
+End Unit_typ_eqb.
+(* End TODO *)
+
+Module Typ.
+
+  Notation index := int (only parsing).
+
+  Inductive type :=
+  | Tindex : index -> type
+  | TZ : type
+  | Tbool : type
+  | Tpositive : type.
+
+  Definition ftype := (list type * type)%type.
+
+  Section Interp.
+
+    Variable t_i : PArray.array typ_eqb.
+
+    Definition interp t :=
+      match t with
+      | Tindex i => (t_i.[i]).(te_carrier)
+      | TZ => Z
+      | Tbool => bool
+      | Tpositive => positive
+      end.
+
+    Definition interp_ftype (t:ftype) :=
+      List.fold_right (fun dom codom =>interp dom -> codom)
+      (interp (snd t)) (fst t).
+
+    (* Boolean equality over interpretation of a btype *)
+    Section Interp_Equality.
+
+      Definition i_eqb (t:type) : interp t -> interp t -> bool :=
+        match t with
+        | Tindex i => (t_i.[i]).(te_eqb)
+        | TZ => Zeq_bool
+        | Tbool => Bool.eqb
+        | Tpositive => Peqb
+        end.
+
+      Lemma i_eqb_spec : forall t x y, i_eqb t x y <-> x = y.
+      Proof.
+       destruct t;simpl;intros.
+       symmetry;apply reflect_iff;apply te_reflect.
+       symmetry;apply Zeq_is_eq_bool.
+       apply Bool.eqb_true_iff.
+       apply Peqb_eq.
+      Qed.
+
+      Lemma reflect_i_eqb : forall t x y, reflect (x = y) (i_eqb t x y).
+      Proof.
+        intros;apply iff_reflect;symmetry;apply i_eqb_spec.
+      Qed.
+
+      Lemma i_eqb_sym : forall t x y, i_eqb t x y = i_eqb t y x.
+      Proof.
+        intros t x y; case_eq (i_eqb t x y); case_eq (i_eqb t y x); auto.
+        change (i_eqb t x y = true) with (is_true (i_eqb t x y)); rewrite i_eqb_spec; intros H1 H2; subst y; pose (H:=reflect_i_eqb t x x); inversion H; [rewrite <- H0 in H1; discriminate|elim H2; auto].
+        change (i_eqb t y x = true) with (is_true (i_eqb t y x)); rewrite i_eqb_spec; intros H1 H2; subst y; pose (H:=reflect_i_eqb t x x); inversion H; [rewrite <- H0 in H2; discriminate|elim H1; auto].
+      Qed.
+
+    End Interp_Equality.
+
+  End Interp.
+
+  (* Plutôt que de tester l'égalité entre deux btypes dans Prop, on
+     écrit une fonction calculant:
+     - si deux btype A et B sont égaux
+     - si oui, une fonction permettant de passer les objets de type A en
+     objets de type B
+     On montre que cette fonction réfléchit l'égalité de Coq. *)
+
+  Section Cast.
+
+  (* L'inductif cast_result spécifie si deux btype sont égaux (Cast) ou
+     non (NoCast). Dans le cas où ils sont égaux, une fonction permet de
+     passer de l'un à l'autre. *)
+
+    Inductive cast_result (A B: type) : Type :=
+    | Cast (k: forall P, P A -> P B)
+    | NoCast.
+
+    Implicit Arguments Cast [A B].
+    Implicit Arguments NoCast [A B].
+
+    Notation idcast := (Cast (fun P x => x)).
+    (* La fonction cast calcule cast_result *)
+
+    Definition cast (A B: type) : cast_result A B :=
+      match A as C, B as D return cast_result C D with
+      | Tindex i, Tindex j =>
+        match cast i j with
+        | Some k => Cast (fun P => k (fun y => P (Tindex y)))
+        | None => NoCast
+        end
+      | TZ, TZ => idcast
+      | Tbool, Tbool => idcast
+      | Tpositive, Tpositive => idcast
+      | _, _ => NoCast
+      end.
+
+    Lemma cast_refl:
+      forall A, cast A A = Cast (fun P (H : P A) => H).
+    Proof.
+      intros A0;destruct A0;simpl;trivial.
+      rewrite cast_refl;trivial.
+    Qed.
+
+    (* Remark : I use this definition because eqb will not be used only in the interpretation *)
+    Definition eqb (A B: type) : bool :=
+      match A, B with
+      | Tindex i, Tindex j => i == j
+      | TZ, TZ => true
+      | Tbool, Tbool => true
+      | Tpositive, Tpositive => true
+      | _, _ => false
+      end.
+
+
+    (* TODO : Move this *)
+    Lemma not_false : ~ false.
+    Proof. intro;discriminate. Qed.
+    Hint Resolve not_false.
+
+    Lemma is_true_true : true.
+    Proof. reflexivity. Qed.
+    Hint Resolve is_true_true.
+
+    Lemma not_is_true_eq_false : forall b:bool, ~ b <-> b = false.
+    Proof. exact not_true_iff_false. Qed.
+
+    Lemma cast_diff: forall A B, eqb A B = false -> cast A B = NoCast.
+    Proof.
+      intros A0 B0;destruct A0; destruct B0;simpl;trivial;try discriminate.
+      intros Heq;rewrite (cast_diff _ _ Heq);trivial.
+    Qed.
+
+    Lemma neq_cast : forall A B,
+      cast A B = (if eqb A B then cast A B else NoCast).
+    Proof.
+      intros C D;case_eq (eqb C D);trivial;apply cast_diff.
+    Qed.
+
+    Lemma reflect_eqb : forall x y, reflect (x = y) (eqb x y).
+    Proof.
+      intros x y;destruct x;destruct y;simpl;try constructor;trivial;try discriminate.
+      apply iff_reflect;rewrite eqb_spec;split;intros H;[inversion H | subst];trivial.
+    Qed.
+
+    Lemma eqb_spec : forall x y, eqb x y <-> x = y.
+    Proof.
+      intros;symmetry;apply reflect_iff;apply reflect_eqb.
+    Qed.
+
+    Lemma eqb_refl : forall x, eqb x x.
+    Proof. intros; rewrite eqb_spec; auto. Qed.
+
+  End Cast.
+
+End Typ.
+
+(* TODO move this *)
+Inductive dlist (A:Type) (P:A->Type) : list A -> Type :=
+| Dnil : dlist A P nil
+| Dcons : forall a l, P a -> dlist A P l -> dlist A P (cons a l).
+
+Set Implicit Arguments.
+Definition list_beq := fun (A : Type) (eq_A : A -> A -> bool) =>
+fix list_eqrec (X Y : list A) : bool :=
+  match X with
+  | nil => match Y with
+           | nil => true
+           | (_ :: _)%list => false
+           end
+  | (x :: x0)%list =>
+      match Y with
+      | nil => false
+      | (x1 :: x2)%list => (eq_A x x1 && list_eqrec x0 x2)%bool
+      end
+  end.
+Unset Implicit Arguments.
+
+Lemma reflect_list_beq : forall (A:Type) (beq:A -> A -> bool),
+  (forall x y, reflect (x = y) (beq x y)) ->
+  forall x y, reflect (x = y) (list_beq beq x y).
+Proof.
+  intros A beq Hbeq;induction x;destruct y;simpl;try (constructor;trivial;discriminate).
+  destruct (Hbeq a a0) as [Heq | Hd];simpl;[ | constructor;intros Heq;elim Hd;inversion Heq;trivial].
+  destruct (IHx y) as [Heq0 | Hd];simpl;[ | constructor;intros Heq0;elim Hd;inversion Heq0;trivial].
+  constructor;subst;trivial.
+Qed.
+
+Lemma list_beq_spec : forall (A:Type) (beq:A -> A -> bool),
+  (forall x y, beq x y <-> x = y) ->
+  forall x y, list_beq beq x y <-> x = y.
+Proof.
+  intros A beq HA x y;symmetry;apply reflect_iff;apply reflect_list_beq.
+  intros;apply iff_reflect;symmetry;apply HA.
+Qed.
+(* End move *)
+
+Module Atom.
+
+  Notation func := int (only parsing).
+ 
+  Inductive cop : Type := 
+   | CO_xH
+   | CO_Z0.
+
+  Inductive unop : Type :=
+   | UO_xO
+   | UO_xI
+   | UO_Zpos 
+   | UO_Zneg
+   | UO_Zopp.
+
+  Inductive binop : Type :=
+   | BO_Zplus
+   | BO_Zminus
+   | BO_Zmult
+   | BO_Zlt
+   | BO_Zle
+   | BO_Zge
+   | BO_Zgt
+   | BO_eq (_ : Typ.type).
+
+  Inductive nop : Type :=
+   | NO_distinct (_ : Typ.type).
+
+  Notation hatom := int (only parsing).
+ 
+  Inductive atom : Type :=
+   | Acop (_: cop)
+   | Auop (_ : unop) (_:hatom)
+   | Abop (_ : binop) (_:hatom) (_:hatom)
+   | Anop (_ : nop) (_: list hatom)
+   | Aapp (_:func) (_: list hatom).
+
+
+  (* Generic predicates and operations *)
+
+  (** Equality *)
+  Definition cop_eqb o o' :=
+   match o, o' with
+   | CO_xH, CO_xH 
+   | CO_Z0, CO_Z0 => true
+   | _,_ => false
+   end.
+
+  Definition uop_eqb o o' :=
+   match o, o' with
+   | UO_xO, UO_xO 
+   | UO_xI, UO_xI
+   | UO_Zpos, UO_Zpos 
+   | UO_Zneg, UO_Zneg
+   | UO_Zopp, UO_Zopp => true
+   | _,_ => false
+   end.
+
+  Definition bop_eqb o o' :=
+   match o, o' with
+   | BO_Zplus, BO_Zplus
+   | BO_Zminus, BO_Zminus
+   | BO_Zmult, BO_Zmult
+   | BO_Zlt, BO_Zlt
+   | BO_Zle, BO_Zle
+   | BO_Zge, BO_Zge
+   | BO_Zgt, BO_Zgt => true
+   | BO_eq t, BO_eq t' => Typ.eqb t t'
+   | _,_ => false
+   end.
+
+  Definition nop_eqb o o' :=
+    match o, o' with
+      | NO_distinct t, NO_distinct t' => Typ.eqb t t'
+    end.
+
+  Definition eqb (t t':atom) :=
+    match t,t' with
+    | Acop o, Acop o' => cop_eqb o o'
+    | Auop o t, Auop o' t' => uop_eqb o o' && (t == t')
+    | Abop o t1 t2, Abop o' t1' t2' => bop_eqb o o' && (t1 == t1') && (t2 == t2')
+    | Anop o t, Anop o' t' => nop_eqb o o' && list_beq Int63Native.eqb t t'
+    | Aapp a la, Aapp b lb => (a == b) && list_beq Int63Native.eqb la lb
+    | _, _ => false
+    end.
+
+  Ltac preflect t :=
+    let Heq := fresh "Heq" in
+      let Hd := fresh "Hd" in
+        destruct t as [Heq | Hd];simpl;
+          [ | constructor;intros Heq;elim Hd;inversion Heq;trivial].
+
+  Lemma reflect_cop_eqb : forall o1 o2, reflect (o1 = o2) (cop_eqb o1 o2).
+  Proof.
+   destruct o1;destruct o2;simpl;constructor;trivial;discriminate.
+  Qed.
+
+  Lemma reflect_uop_eqb : forall o1 o2, reflect (o1 = o2) (uop_eqb o1 o2).
+  Proof.
+   destruct o1;destruct o2;simpl;constructor;trivial;discriminate.
+  Qed.
+ 
+  Lemma reflect_bop_eqb : forall o1 o2, reflect (o1 = o2) (bop_eqb o1 o2).
+  Proof.
+   destruct o1;destruct o2;simpl;try (constructor;trivial;discriminate).
+   preflect (Typ.reflect_eqb t t0).
+   constructor;subst;trivial.
+  Qed.
+
+  Lemma reflect_nop_eqb : forall o1 o2, reflect (o1 = o2) (nop_eqb o1 o2).
+  Proof.
+    intros [t1] [t2]; simpl; preflect (Typ.reflect_eqb t1 t2); constructor; subst; reflexivity.
+  Qed.
+
+  Lemma reflect_eqb : forall t1 t2, reflect (t1 = t2) (eqb t1 t2).
+  Proof.
+    destruct t1;destruct t2;simpl; try (constructor;trivial;discriminate).
+    (* Constants *)
+    preflect (reflect_cop_eqb c c0);constructor;subst;trivial.
+    (* Unary operators *)
+    preflect (reflect_uop_eqb u u0); preflect (Int63Properties.reflect_eqb i i0);
+      constructor;subst;trivial.
+    (* Binary operators *)
+    preflect (reflect_bop_eqb b b0); 
+    preflect (Int63Properties.reflect_eqb i i1);
+    preflect (Int63Properties.reflect_eqb i0 i2);
+    constructor;subst;trivial.
+    (* N-ary operators *)
+    preflect (reflect_nop_eqb n n0); preflect (reflect_list_beq _ _ Int63Properties.reflect_eqb l l0); constructor; subst; reflexivity.
+    (* Application *)
+    preflect (Int63Properties.reflect_eqb i i0);
+    preflect (reflect_list_beq _ _ Int63Properties.reflect_eqb l l0);
+    constructor;subst;trivial.
+  Qed.
+  
+  Lemma eqb_spec : forall t1 t2, eqb t1 t2 <-> t1 = t2.
+  Proof.
+    intros;symmetry;apply reflect_iff;apply reflect_eqb.
+  Qed.
+  
+  (** Typing and interpretation *)
+  
+  Record val (t:Type) (I:t -> Type) := Val {
+    v_type : t;
+    v_val : I v_type
+  }.
+
+  Section Typing_Interp.
+    Variable t_i : PArray.array typ_eqb.
+
+    Local Notation interp_t := (Typ.interp t_i).
+    Local Notation interp_ft := (Typ.interp_ftype t_i).
+
+    Definition bval := val Typ.type interp_t.
+    Definition Bval := Val Typ.type interp_t.
+    Definition tval := val Typ.ftype interp_ft.
+    Definition Tval := Val Typ.ftype interp_ft.
+
+    Definition bvtrue : bval := Bval Typ.Tbool true.
+    Definition bvfalse : bval := Bval Typ.Tbool false.
+
+    Lemma Bval_inj1 : forall T U t u, Bval T t = Bval U u -> T = U.
+    Proof. intros T U t u H; inversion H; auto. Qed.
+
+    Lemma Bval_inj2 : forall T t u, Bval T t = Bval T u -> t = u.
+    Proof.
+      intros T t u H; assert (H1: (fun (x:bval) =>
+      match Typ.cast (v_type _ _ x) T with
+        | Typ.Cast k => k _ (v_val _ _ x) = v_val _ _ (Bval T u)
+        | Typ.NoCast => True
+      end) (Bval T t)).
+      rewrite H, Typ.cast_refl; reflexivity.
+      simpl in H1; rewrite Typ.cast_refl in H1; auto.
+    Qed.
+
+    (* Interprétation d'une fonction*)
+    Variable t_func : PArray.array tval.
+
+    (** Type checking of atom assuming an type for hatom *)
+    Section Typ_Aux.
+      Variable get_type : hatom -> Typ.type.
+
+      Definition typ_cop o := 
+        match o with
+        | CO_xH => Typ.Tpositive 
+        | CO_Z0 => Typ.TZ
+        end.
+
+      Definition typ_uop o :=
+        match o with
+        | UO_xO => (Typ.Tpositive,Typ.Tpositive) 
+        | UO_xI => (Typ.Tpositive,Typ.Tpositive) 
+        | UO_Zpos => (Typ.Tpositive, Typ.TZ)
+        | UO_Zneg => (Typ.Tpositive, Typ.TZ)
+        | UO_Zopp => (Typ.TZ, Typ.TZ)
+        end.
+
+      Definition typ_bop o := 
+        match o with
+        | BO_Zplus  => ((Typ.TZ,Typ.TZ), Typ.TZ) 
+        | BO_Zminus => ((Typ.TZ,Typ.TZ), Typ.TZ) 
+        | BO_Zmult  => ((Typ.TZ,Typ.TZ), Typ.TZ) 
+        | BO_Zlt    => ((Typ.TZ,Typ.TZ), Typ.Tbool) 
+        | BO_Zle    => ((Typ.TZ,Typ.TZ), Typ.Tbool) 
+        | BO_Zge    => ((Typ.TZ,Typ.TZ), Typ.Tbool) 
+        | BO_Zgt    => ((Typ.TZ,Typ.TZ), Typ.Tbool)
+        | BO_eq t   => ((t,t),Typ.Tbool)
+        end.
+
+      Definition typ_nop o :=
+        match o with
+          | NO_distinct t => (t,Typ.Tbool)
+        end.
+
+      Fixpoint check_args (args:list hatom) (targs:list Typ.type) :=
+        match args, targs with
+        | nil, nil => true
+        | a::args, t::targs => Typ.eqb (get_type a) t && check_args args targs
+        | _, _ => false
+        end.
+
+      Definition check_aux (a:atom) (t:Typ.type) : bool := 
+        match a with
+        | Acop o => Typ.eqb (typ_cop o) t 
+        | Auop o a =>
+          let (ta,t') := typ_uop o in
+          Typ.eqb t' t && Typ.eqb (get_type a) ta
+        | Abop o a1 a2 =>
+          let (ta,t') := typ_bop o in
+          let (ta1,ta2) := ta in
+          Typ.eqb t' t && Typ.eqb (get_type a1) ta1 && Typ.eqb (get_type a2) ta2 
+        | Anop o a =>
+          let (ta,t') := typ_nop o in
+          (Typ.eqb t' t) && (List.forallb (fun t1 => Typ.eqb (get_type t1) ta) a)
+        | Aapp f args =>
+          let (targs,tr) := v_type _ _ (t_func.[f]) in
+          check_args args targs && Typ.eqb tr t
+        end.
+
+      (* Typing is unique *)
+
+      Lemma unicity : forall a t1 t2,
+        check_aux a t1 -> check_aux a t2 -> t1 = t2.
+      Proof.
+        destruct a;simpl. 
+        (* Constants *)
+        intros t1 t2;rewrite !Typ.eqb_spec;intros;subst;trivial.
+        (* Unary operators *)
+        unfold is_true; intros t1 t2;rewrite (surjective_pairing (typ_uop u)),!andb_true_iff.
+        intros [H1 _] [H2 _]; change (is_true (Typ.eqb (snd (typ_uop u)) t1)) in H1.
+        change (is_true (Typ.eqb (snd (typ_uop u)) t2)) in H2.
+        rewrite Typ.eqb_spec in H1, H2;subst;trivial.
+        (* Binary operators *)
+        unfold is_true; intros t1 t2;rewrite (surjective_pairing (typ_bop b)),
+           (surjective_pairing (fst (typ_bop b))) ,!andb_true_iff.
+        intros [[H1 _] _] [[H2 _] _]; change (is_true (Typ.eqb (snd (typ_bop b)) t1)) in H1.
+        change (is_true (Typ.eqb (snd (typ_bop b)) t2)) in H2.
+        rewrite Typ.eqb_spec in H1, H2;subst;trivial.
+        (* N-ary operators *)
+        intros t1 t2; destruct (typ_nop n) as [ta t']; unfold is_true; rewrite !andb_true_iff; change (is_true (Typ.eqb t' t1) /\ is_true (List.forallb (fun t3 : int => Typ.eqb (get_type t3) ta) l) -> is_true (Typ.eqb t' t2) /\ is_true (List.forallb (fun t3 : int => Typ.eqb (get_type t3) ta) l) -> t1 = t2); rewrite !Typ.eqb_spec; intros [H1 _] [H2 _]; subst; auto.
+        (* Application *)
+        intros t1 t2;destruct (v_type Typ.ftype interp_ft (t_func.[ i])).
+        unfold is_true;rewrite !andb_true_iff;intros [_ H1] [_ H2].
+        transitivity t;[ symmetry| ];rewrite <-Typ.eqb_spec;trivial.
+      Qed.
+
+      (* Typing is decidable *)
+
+      Lemma check_args_dec : forall tr args targs,
+        {exists T : Typ.type,
+          check_args args targs && Typ.eqb tr T} +
+        {forall T : Typ.type,
+          check_args args targs && Typ.eqb tr T = false}.
+      Proof.
+        intro A; induction args as [ |h l IHl]; simpl.
+        (* Base case *)
+        intros [ | ]; simpl.
+        left; exists A; apply Typ.eqb_refl.
+        intros; right; reflexivity.
+        (* Inductive case *)
+        intros [ |B targs]; simpl.
+        right; reflexivity.
+        case (Typ.eqb (get_type h) B); simpl; auto.
+      Qed.
+
+      Lemma check_aux_dec : forall a,
+        {exists T, check_aux a T} + {forall T, check_aux a T = false}.
+      Proof.
+        intros [op|op h|op h1 h2|op ha|f args]; simpl.
+        (* Constants *)
+        left; destruct op; simpl.
+        exists Typ.Tpositive; auto.
+        exists Typ.TZ; auto.
+        (* Unary operators *)
+        destruct op; simpl; try (case (Typ.eqb (get_type h) Typ.Tpositive); [left; exists Typ.Tpositive|right; intro; rewrite andb_false_r]; reflexivity); try (case (Typ.eqb (get_type h) Typ.Tpositive); [left; exists Typ.TZ|right; intro; rewrite andb_false_r]; reflexivity); case (Typ.eqb (get_type h) Typ.TZ); [left; exists Typ.TZ|right; intro; rewrite andb_false_r]; reflexivity.
+        (* Binary operators *)
+        destruct op; simpl; try (case (Typ.eqb (get_type h1) Typ.TZ); [case (Typ.eqb (get_type h2) Typ.TZ); [left; exists Typ.TZ|right; intro; rewrite andb_false_r]|right; intro; rewrite andb_false_r]; reflexivity); try (case (Typ.eqb (get_type h1) Typ.TZ); [case (Typ.eqb (get_type h2) Typ.TZ); [left; exists Typ.Tbool|right; intro; rewrite andb_false_r]|right; intro; rewrite andb_false_r]; reflexivity); case (Typ.eqb (get_type h1) t); [case (Typ.eqb (get_type h2) t); [left; exists Typ.Tbool|right; intro; rewrite andb_false_r]|right; intro; rewrite andb_false_r]; reflexivity.
+        (* N-ary operators *)
+        destruct op as [ty]; simpl; case (List.forallb (fun t1 : int => Typ.eqb (get_type t1) ty) ha).
+        left; exists Typ.Tbool; auto.
+        right; intro T; rewrite andb_false_r; auto.
+        (* Application *)
+        case (v_type Typ.ftype interp_ft (t_func .[ f])); intros; apply check_args_dec.
+      Qed.
+
+    End Typ_Aux.
+    (** Interpretation of hatom assuming an interpretation for atom *)
+    Section Interp_Aux.
+
+      Variable interp_hatom : hatom -> bval.
+
+      Definition apply_unop (t  r : Typ.type)
+            (op : interp_t t -> interp_t r) (tv:bval) :=
+        let (t', v) := tv in
+        match Typ.cast t' t with
+        | Typ.Cast k => Bval r (op (k _ v))
+        | _ => bvtrue
+        end.
+
+      Definition apply_binop (t1 t2 r : Typ.type)
+            (op : interp_t t1 -> interp_t t2 -> interp_t r) (tv1 tv2:bval) :=
+        let (t1', v1) := tv1 in
+        let (t2', v2) := tv2 in
+        match Typ.cast t1' t1, Typ.cast t2' t2 with
+        | Typ.Cast k1, Typ.Cast k2 => Bval r (op (k1 _ v1) (k2 _ v2))
+        | _, _ => bvtrue
+        end.
+
+      Fixpoint apply_func
+           targs tr (f:interp_ft (targs,tr)) (lv:list bval) : bval :=
+        match targs as targs0 return interp_ft (targs0,tr) -> bval with
+        | nil => fun v =>
+          match lv with
+          | nil => Bval tr v
+          | _ => bvtrue
+          end
+        | t::targs => fun f =>
+          match lv with
+          | v::lv =>
+            let (tv,v) := v in
+            match Typ.cast tv t with
+            | Typ.Cast k =>
+              let f := f (k _ v) in apply_func targs tr f lv
+            | _ => bvtrue
+            end
+          | _ => bvtrue
+          end
+        end f.
+
+      Definition interp_cop o :=
+        match o with
+        | CO_xH => Bval Typ.Tpositive xH
+        | CO_Z0 => Bval Typ.TZ Z0
+        end.
+
+      Definition interp_uop o :=    
+        match o with
+        | UO_xO   => apply_unop Typ.Tpositive Typ.Tpositive xO
+        | UO_xI   => apply_unop Typ.Tpositive Typ.Tpositive xI
+        | UO_Zpos => apply_unop Typ.Tpositive Typ.TZ Zpos
+        | UO_Zneg => apply_unop Typ.Tpositive Typ.TZ Zneg
+        | UO_Zopp => apply_unop Typ.TZ Typ.TZ Zopp
+        end.
+
+      Definition interp_bop o :=
+         match o with
+         | BO_Zplus => apply_binop Typ.TZ Typ.TZ Typ.TZ Zplus
+         | BO_Zminus => apply_binop Typ.TZ Typ.TZ Typ.TZ Zminus
+         | BO_Zmult => apply_binop Typ.TZ Typ.TZ Typ.TZ Zmult
+         | BO_Zlt => apply_binop Typ.TZ Typ.TZ Typ.Tbool Zlt_bool
+         | BO_Zle => apply_binop Typ.TZ Typ.TZ Typ.Tbool Zle_bool
+         | BO_Zge => apply_binop Typ.TZ Typ.TZ Typ.Tbool Zge_bool
+         | BO_Zgt => apply_binop Typ.TZ Typ.TZ Typ.Tbool Zgt_bool
+         | BO_eq t => apply_binop t t Typ.Tbool (Typ.i_eqb t_i t)
+         end.
+
+      Fixpoint compute_interp ty acc l :=
+        match l with
+          | nil => Some acc
+          | a::q =>
+            let (ta,va) := interp_hatom a in
+            match Typ.cast ta ty with
+              | Typ.Cast ka => compute_interp ty ((ka _ va)::acc) q
+              | _ => None
+            end
+        end.
+
+      (* Lemma compute_interp_spec : forall ty l acc, *)
+      (*   match compute_interp ty acc l with *)
+      (*     | Some l' => forall i, In i l' <-> (In i acc \/ (exists a, In a l /\ interp_hatom a = Bval ty i)) *)
+      (*     | None => exists a, In a l /\ let (ta,_) := interp_hatom a in ta <> ty *)
+      (*   end. *)
+      (* Proof. *)
+      (*   intro ty; induction l as [ |a q IHq]; simpl. *)
+      (*   intros acc i; split. *)
+      (*   intro H; left; auto. *)
+      (*   intros [H|[a [H _]]]; auto; elim H. *)
+      (*   intro acc; case_eq (interp_hatom a); intros ta va Heq; rewrite Typ.neq_cast; case_eq (Typ.eqb ta ty). *)
+      (*   change (Typ.eqb ta ty = true) with (is_true (Typ.eqb ta ty)); rewrite Typ.eqb_spec; intro; subst ta; rewrite Typ.cast_refl; generalize (IHq (va :: acc)); clear IHq; case (compute_interp ty (va :: acc) q). *)
+      (*   intros l IH i; rewrite (IH i); clear IH; split; intros [H|[a1 [H1 H2]]]. *)
+      (*   inversion H; auto. *)
+      (*   subst va; clear H; right; exists a; split; auto. *)
+      (*   right; exists a1; split; auto. *)
+      (*   left; constructor 2; auto. *)
+      (*   destruct H1 as [H1|H1]. *)
+      (*   subst a1; left; constructor 1; rewrite Heq in H2; apply (Bval_inj2 ty); auto. *)
+      (*   right; exists a1; auto. *)
+      (*   intros [a1 [H1 H2]]; exists a1; split; auto. *)
+      (*   intro H; exists a; split; auto; rewrite Heq; intro H1; subst ta; rewrite Typ.eqb_refl in H; discriminate. *)
+      (* Qed. *)
+
+      Lemma compute_interp_spec : forall ty l acc,
+        match compute_interp ty acc l with
+          | Some l' => forall i j, In2 i j l' <-> (In2 i j acc \/ (In j acc /\ exists a, In a l /\ interp_hatom a = Bval ty i) \/ (exists a b, In2 b a l /\ interp_hatom a = Bval ty i /\ interp_hatom b = Bval ty j))
+          | None => exists a, In a l /\ let (ta,_) := interp_hatom a in ta <> ty
+        end.
+      Proof.
+        intro ty; induction l as [ |a q IHq]; simpl.
+        intros acc i; split.
+        intro H; left; auto.
+        intros [H|[[_ [a [H _]]]|[a [b [H _]]]]]; auto.
+        elim H.
+        inversion H.
+        intro acc; case_eq (interp_hatom a); intros ta va Heq; rewrite Typ.neq_cast; case_eq (Typ.eqb ta ty).
+        change (Typ.eqb ta ty = true) with (is_true (Typ.eqb ta ty)); rewrite Typ.eqb_spec; intro; subst ta; rewrite Typ.cast_refl; generalize (IHq (va :: acc)); clear IHq; case (compute_interp ty (va :: acc) q).
+        intros l IH i j; rewrite (IH i j); clear IH; split.
+        intros [H|[[H [b [H1 H2]]]|[b [c [H [H1 H2]]]]]].
+        inversion H; clear H.
+        subst i l0; right; left; split; auto; exists a; split; auto.
+        subst k l0; left; auto.
+        inversion H; clear H.
+        subst va; right; right; exists b; exists a; repeat split; auto; constructor 1; auto.
+        right; left; split; auto; exists b; auto.
+        right; right; exists b; exists c; repeat split; auto; constructor 2; auto.
+        intros [H|[[H [b [[H1|H1] H2]]]|[b [c [H [H1 H2]]]]]].
+        left; constructor 2; auto.
+        subst b; rewrite Heq in H2; generalize (Bval_inj2 _ _ _ H2); intro; subst va; left; constructor; auto.
+        right; left; split.
+        constructor 2; auto.
+        exists b; auto.
+        inversion H; clear H.
+        subst c l0; rewrite Heq in H2; generalize (Bval_inj2 _ _ _ H2); intro; subst va; right; left; split.
+        constructor 1; auto.
+        exists b; auto.
+        subst k l0; right; right; exists b; exists c; auto.
+        intros [a1 [H1 H2]]; exists a1; split; auto.
+        intro H; exists a; split; auto; rewrite Heq; intro H1; subst ta; rewrite Typ.eqb_refl in H; discriminate.
+      Qed.
+
+      (* Lemma compute_interp_spec_rev : forall ty l, *)
+      (*   match compute_interp ty nil l with *)
+      (*     | Some l' => forall i, In i (rev l') <-> (exists a, In a l /\ interp_hatom a = Bval ty i) *)
+      (*     | None => exists a, In a l /\ let (ta,_) := interp_hatom a in ta <> ty *)
+      (*   end. *)
+      (* Proof. (* ICI *) *)
+      (*   intros ty l; generalize (compute_interp_spec ty l nil); case (compute_interp ty nil l); auto; intros l' H i; rewrite <- In_rev, (H i); split; auto; intros [H1|H1]; auto; inversion H1. *)
+      (* Qed. *)
+
+      Lemma compute_interp_spec_rev : forall ty l,
+        match compute_interp ty nil l with
+          | Some l' => forall i j, In2 j i (rev l') <-> (exists a b, In2 b a l /\ interp_hatom a = Bval ty i /\ interp_hatom b = Bval ty j)
+          | None => exists a, In a l /\ let (ta,_) := interp_hatom a in ta <> ty
+        end.
+      Proof.
+        intros ty l; generalize (compute_interp_spec ty l nil); case (compute_interp ty nil l); auto; intros l' H i j; rewrite In2_rev, (H i j); split; auto; intros [H1|[[H1 _]|H1]]; auto; inversion H1.
+      Qed.
+
+      Definition interp_aux (a:atom) : bval :=
+        match a with
+        | Acop o => interp_cop o
+        | Auop o a => interp_uop o (interp_hatom a)
+        | Abop o a1 a2 => interp_bop o (interp_hatom a1) (interp_hatom a2)
+        | Anop (NO_distinct t) a =>
+          match compute_interp t nil a with
+            | Some l => Bval Typ.Tbool (distinct (Typ.i_eqb t_i t) (rev l))
+            | None => bvtrue
+          end
+        | Aapp f args =>
+          let (tf,f) := t_func.[f] in
+          let lv := List.map interp_hatom args in
+          apply_func (fst tf) (snd tf) f lv
+        end.
+
+      Definition interp_bool (v:bval) : bool :=
+        let (t,v) := v in
+        match Typ.cast t Typ.Tbool with
+        | Typ.Cast k => k _ v
+        | _ => true
+        end.
+
+
+      (* If an atom is well-typed, it has an interpretation *)
+
+      Variable get_type : hatom -> Typ.type.
+      Hypothesis check_aux_interp_hatom : forall h,
+        exists v, interp_hatom h = (Bval (get_type h) v).
+
+      Lemma check_args_interp_aux : forall t l f,
+        (let (targs, tr) := v_type Typ.ftype interp_ft f in
+          check_args get_type l targs && Typ.eqb tr t) ->
+        exists v : interp_t t,
+          (let (tf, f0) := f in
+            apply_func (fst tf) (snd tf) f0 (List.map interp_hatom l)) =
+          Bval t v.
+      Proof.
+        intro A; induction l as [ |h l IHl]; simpl; intros [tf f]; simpl.
+        (* Base case *)
+        destruct tf as [[ | ] tr]; try discriminate; simpl; rewrite Typ.eqb_spec; intro; subst tr; exists f; auto.
+        (* Inductive case *)
+        destruct tf as [[ |B targs] tr]; try discriminate; simpl; rewrite <- andb_assoc; unfold is_true; rewrite andb_true_iff; change (Typ.eqb (get_type h) B = true /\ check_args get_type l targs && Typ.eqb tr A = true) with (is_true (Typ.eqb (get_type h) B) /\ is_true (check_args get_type l targs && Typ.eqb tr A)); rewrite Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h) as [v0 Heq0]; rewrite Heq0; generalize v0 Heq0; rewrite H1; intros v1 Heq1; simpl; generalize (IHl (Tval (targs,tr) (f v1))); simpl; intro IH; destruct (IH H2) as [v2 Heq2]; exists v2; rewrite Typ.cast_refl; auto.
+      Qed.
+
+      Lemma check_aux_interp_aux_aux : forall a t,
+         check_aux get_type a t ->
+         exists v, interp_aux a = (Bval t v).
+      Proof.
+        intros [op|op h|op h1 h2|op ha|f l]; simpl.
+        (* Constants *)
+        destruct op; intros [i| | | ]; simpl; try discriminate; intros _.
+        exists 1%positive; auto.
+        exists 0%Z; auto.
+        (* Unary operators *)
+        destruct op; intros [i| | | ]; simpl; try discriminate; rewrite Typ.eqb_spec; intro H1; destruct (check_aux_interp_hatom h) as [x Hx]; rewrite Hx; simpl; generalize x Hx; rewrite H1; intros y Hy; rewrite Typ.cast_refl.
+        exists (y~0)%positive; auto.
+        exists (y~1)%positive; auto.
+        exists (Zpos y); auto.
+        exists (Zneg y); auto.
+        exists (- y)%Z; auto.
+        (* Binary operators *)
+        destruct op as [ | | | | | | |A]; intros [i| | | ]; simpl; try discriminate; unfold is_true; rewrite andb_true_iff; try (change (Typ.eqb (get_type h1) Typ.TZ = true /\ Typ.eqb (get_type h2) Typ.TZ = true) with (is_true (Typ.eqb (get_type h1) Typ.TZ) /\ is_true (Typ.eqb (get_type h2) Typ.TZ)); rewrite !Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h1) as [x1 Hx1]; rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl; generalize x1 Hx1 x2 Hx2; rewrite H1, H2; intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl).
+        exists (y1 + y2)%Z; auto.
+        exists (y1 - y2)%Z; auto.
+        exists (y1 * y2)%Z; auto.
+        exists (y1 <? y2)%Z; auto.
+        exists (y1 <=? y2)%Z; auto.
+        exists (y1 >=? y2)%Z; auto.
+        exists (y1 >? y2)%Z; auto.
+        change (Typ.eqb (get_type h1) A = true /\ Typ.eqb (get_type h2) A = true) with (is_true (Typ.eqb (get_type h1) A) /\ is_true (Typ.eqb (get_type h2) A)); rewrite !Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h1) as [x1 Hx1]; rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl; generalize x1 Hx1 x2 Hx2; rewrite H1, H2; intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl; exists (Typ.i_eqb t_i A y1 y2); auto.
+        (* N-ary operators *)
+        destruct op as [A]; simpl; intros [ | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha).
+        intro l; exists (distinct (Typ.i_eqb t_i A) (rev l)); auto.
+        exists true; auto.
+        (* Application *)
+        intro t; apply check_args_interp_aux.
+      Qed.
+
+
+      (* If an atom is not well-typed, its interpretation is bvtrue *)
+
+      Lemma check_args_interp_aux_contr : forall l f,
+        (forall T : Typ.type,
+          (let (targs, tr) := v_type Typ.ftype interp_ft f in
+            check_args get_type l targs && Typ.eqb tr T) = false) ->
+        (let (tf, f0) := f in
+          apply_func (fst tf) (snd tf) f0 (List.map interp_hatom l)) = bvtrue.
+        induction l as [ |h l IHl]; simpl; intros [tf f]; simpl.
+        (* Base case *)
+        destruct tf as [[ | ] tr]; simpl; auto; intro H; generalize (H tr); rewrite Typ.eqb_refl; discriminate.
+        (* Inductive case *)
+        destruct tf as [[ |B targs] tr]; simpl; auto. intro H. destruct (check_aux_interp_hatom h) as [v Hv]. rewrite Hv. simpl. assert (H2: (Typ.eqb (get_type h) B = false) \/ (forall T : Typ.type, check_args get_type l targs && Typ.eqb tr T = false)) by (case_eq (Typ.eqb (get_type h) B); try (intros; left; reflexivity); intro Heq; right; intro T; generalize (H T); rewrite Heq; auto). destruct H2 as [H2|H2]; rewrite Typ.neq_cast.
+        rewrite H2. auto.
+        case_eq (Typ.eqb (get_type h) B); auto. change (Typ.eqb (get_type h) B = true) with (is_true (Typ.eqb (get_type h) B)). rewrite Typ.eqb_spec. intro; subst B. rewrite Typ.cast_refl. apply (IHl (Tval (targs,tr) (f v))). auto.
+      Qed.
+
+      Lemma check_aux_interp_aux_contr_aux : forall a,
+        (forall T, check_aux get_type a T = false) ->
+        interp_aux a = bvtrue.
+      Proof.
+        intros [op|op h|op h1 h2|op ha|f l]; simpl.
+        (* Constants *)
+        destruct op; simpl; intro H.
+        discriminate (H Typ.Tpositive).
+        discriminate (H Typ.TZ).
+        (* Unary operators *)
+        destruct op; simpl; intro H; destruct (check_aux_interp_hatom h) as [v Hv]; rewrite Hv; simpl; rewrite Typ.neq_cast; try (pose (H2 := H Typ.Tpositive); simpl in H2; rewrite H2; auto); pose (H2 := H Typ.TZ); simpl in H2; rewrite H2; auto.
+        (* Binary operators *)
+        destruct op; simpl; intro H; destruct (check_aux_interp_hatom h1) as [v1 Hv1]; destruct (check_aux_interp_hatom h2) as [v2 Hv2]; rewrite Hv1, Hv2; simpl; try (pose (H2 := H Typ.TZ); simpl in H2; rewrite andb_false_iff in H2; destruct H2 as [H2|H2]; [rewrite (Typ.neq_cast (get_type h1)), H2|rewrite (Typ.neq_cast (get_type h2)), H2; case (Typ.cast (get_type h1) Typ.TZ)]; auto); try (pose (H2 := H Typ.Tbool); simpl in H2; rewrite andb_false_iff in H2; destruct H2 as [H2|H2]; [rewrite (Typ.neq_cast (get_type h1)), H2|rewrite (Typ.neq_cast (get_type h2)), H2; case (Typ.cast (get_type h1) Typ.TZ)]; auto); case (Typ.cast (get_type h1) t); auto.
+        (* N-ary operators *)
+        destruct op as [A]; simpl; intro H; generalize (H Typ.Tbool); simpl; clear H; assert (H: forall l1, List.forallb (fun t1 : int => Typ.eqb (get_type t1) A) ha = false -> match compute_interp A l1 ha with | Some l => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l)) | None => bvtrue end = bvtrue).
+        induction ha as [ |h ha Iha]; simpl.
+        intros; discriminate.
+        intro l1; destruct (check_aux_interp_hatom h) as [vh Hh]; case_eq (Typ.eqb (get_type h) A); simpl.
+        change (Typ.eqb (get_type h) A = true) with (is_true (Typ.eqb (get_type h) A)); rewrite Typ.eqb_spec; intro; subst A; intro H; rewrite Hh; simpl; rewrite Typ.cast_refl; apply Iha; auto.
+        intros H _; rewrite Hh; simpl; rewrite (Typ.cast_diff _ _ H); auto.
+        apply H.
+        (* Application *)
+        apply check_args_interp_aux_contr.
+      Qed.
+
+    End Interp_Aux.
+
+    Section Interp_get.
+
+      Variable t_atom : PArray.array atom.
+
+      Definition t_interp : PArray.array bval :=
+        PArray.foldi_left (fun i t_a a => t_a.[i <- interp_aux (PArray.get t_a) a])
+          (PArray.make (PArray.length t_atom) (interp_cop CO_xH)) t_atom.
+
+      Definition lt_atom i a :=
+        match a with
+        | Acop _ => true
+        | Auop _ h => h < i
+        | Abop _ h1 h2 => (h1 < i) && (h2 < i)
+        | Anop _ ha => List.forallb (fun h => h < i) ha
+        | Aapp f args => List.forallb (fun h => h < i) args
+        end.
+
+      Lemma lt_interp_aux :
+         forall f1 f2 i, (forall j, j < i -> f1 j = f2 j) ->
+         forall a, lt_atom i a ->
+             interp_aux f1 a = interp_aux f2 a.
+      Proof.
+        intros f1 f2 i Hf; destruct a;simpl;intros;auto.
+        (* Unary operators *)
+        rewrite Hf;trivial.
+        (* Binary operators *)
+        unfold is_true in H;rewrite andb_true_iff in H;destruct H;rewrite !Hf;trivial.
+        (* N-ary operators *)
+        destruct n as [A]; replace (compute_interp f1 A nil l) with (compute_interp f2 A nil l); trivial; assert (H1: forall acc, compute_interp f2 A acc l = compute_interp f1 A acc l); auto; induction l as [ |k l IHl]; simpl; auto; intro acc; simpl in H; unfold is_true in H; rewrite andb_true_iff in H; destruct H as [H1 H2]; rewrite (Hf _ H1); destruct (f2 k) as [ta va]; destruct (Typ.cast ta A) as [ka| ]; auto.
+        (* Application *)
+        replace (List.map f1 l) with (List.map f2 l); trivial.
+        induction l;simpl in H |- *;trivial.
+        unfold is_true in H;rewrite andb_true_iff in H;destruct H;rewrite Hf, IHl;trivial.
+      Qed.
+
+      Definition wf := PArray.forallbi lt_atom t_atom.
+
+      Hypothesis wf_t_i : wf.
+
+      Lemma length_t_interp : length t_interp = length t_atom.
+      Proof.
+        unfold t_interp;apply PArray.foldi_left_Ind with
+          (P := fun i a => length a = length t_atom).
+        intros;rewrite length_set;trivial.
+        rewrite length_make, ltb_length;trivial.
+      Qed.
+
+      Lemma default_t_interp : default t_interp = interp_cop CO_xH.
+      Proof.
+        unfold t_interp;apply PArray.foldi_left_Ind with
+          (P := fun i a => default a = interp_cop CO_xH).
+        intros;rewrite default_set;trivial.
+        apply default_make.
+      Qed.
+
+      Lemma t_interp_wf_lt : forall i, i < PArray.length t_atom ->
+         t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]).
+      Proof.
+        set (P' i t := length t = length t_atom ->
+               forall j, j < i ->
+               t.[j] = interp_aux (PArray.get t) (t_atom.[j])).
+        assert (P' (length t_atom) t_interp).
+         unfold is_true, wf in wf_t_i;rewrite PArray.forallbi_spec in wf_t_i.
+         unfold t_interp;apply foldi_left_Ind;unfold P';intros.
+         rewrite length_set in H1.
+         destruct (Int63Properties.reflect_eqb j i).
+          rewrite e, PArray.get_set_same.
+          apply lt_interp_aux with (2:= wf_t_i i H).
+          intros;rewrite get_set_other;trivial.
+          intros Heq;elim (not_ltb_refl i);rewrite Heq at 1;trivial.
+          rewrite H1;trivial.
+         assert (j < i).
+          assert ([|j|] <> [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial).
+          generalize H2;unfold is_true;rewrite !ltb_spec,
+            (to_Z_add_1 _ _ H);auto with zarith.
+         rewrite get_set_other, H0;auto.
+         apply lt_interp_aux with (2:= wf_t_i j (ltb_trans _ _ _ H3 H)).
+         intros;rewrite get_set_other;trivial.
+         intros Heq;elim (not_ltb_refl i);apply ltb_trans with j;
+           [ rewrite Heq| ];trivial.
+         elim (ltb_0 _ H0).
+        apply H;apply length_t_interp.
+      Qed.
+
+      Hypothesis default_t_atom : default t_atom = Acop CO_xH.
+
+      Lemma t_interp_wf : forall i,
+         t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]).
+      Proof.
+        intros i;case_eq (i< PArray.length t_atom);intros.
+        apply t_interp_wf_lt;trivial.
+        rewrite !PArray.get_outofbound;trivial.
+        rewrite default_t_atom, default_t_interp;trivial.
+        rewrite length_t_interp;trivial.
+      Qed.
+
+      Definition get_type' (t_interp':array bval) i := v_type _ _ (t_interp'.[i]).
+
+      Local Notation get_type := (get_type' t_interp).
+
+      (* If an atom is well-typed, it has an interpretation *)
+
+      Lemma check_aux_interp_aux_lt_aux : forall a h,
+        (forall j : int,
+          j < h ->
+          exists v : interp_t (v_type Typ.type interp_t (a .[ j])),
+            a .[ j] = Bval (v_type Typ.type interp_t (a .[ j])) v) ->
+        forall l, List.forallb (fun h0 : int => h0 < h) l = true ->
+          forall (f0: tval),
+            exists
+              v : interp_t
+              (v_type Typ.type interp_t
+                (let (tf, f) := f0 in
+                  apply_func (fst tf) (snd tf) f (List.map (get a) l))),
+              (let (tf, f) := f0 in
+                apply_func (fst tf) (snd tf) f (List.map (get a) l)) =
+              Bval
+              (v_type Typ.type interp_t
+                (let (tf, f) := f0 in
+                  apply_func (fst tf) (snd tf) f (List.map (get a) l))) v.
+      Proof.
+        intros a h IH; induction l as [ |j l IHl]; simpl.
+        intros _ [[[ | ] tr] f]; simpl.
+        exists f; auto.
+        exists true; auto.
+        rewrite andb_true_iff; intros [H1 H2] [[[ |A targs] tr] f]; simpl.
+        exists true; auto.
+        destruct (IH j H1) as [x Hx]; rewrite Hx; simpl; case (Typ.cast (v_type Typ.type interp_t (a .[ j])) A); simpl.
+        intro k; destruct (IHl H2 (Tval (targs,tr) (f (k interp_t x)))) as [y Hy]; simpl in Hy; rewrite Hy; simpl; exists y; auto.
+        exists true; auto.
+      Qed.
+
+      Lemma check_aux_interp_aux_lt : forall h, h < length t_atom ->
+        forall a,
+          (forall j, j < h ->
+            exists v, a.[j] = Bval (v_type _ _ (a.[j])) v) ->
+          exists v, interp_aux (get a) (t_atom.[h]) =
+            Bval (v_type _ _ (interp_aux (get a) (t_atom.[h]))) v.
+      Proof.
+        unfold wf, is_true in wf_t_i; rewrite forallbi_spec in wf_t_i.
+        intros h Hh a IH; generalize (wf_t_i h Hh).
+        case (t_atom.[h]); simpl.
+        (* Constants *)
+        intros [ | ] _; simpl.
+        exists 1%positive; auto.
+        exists 0%Z; auto.
+        (* Unary operators *)
+        intros [ | | | | ] i H; simpl; destruct (IH i H) as [x Hx]; rewrite Hx; simpl.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.Tpositive); simpl; try (exists true; auto); intro k; exists ((k interp_t x)~0)%positive; auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.Tpositive); simpl; try (exists true; auto); intro k; exists ((k interp_t x)~1)%positive; auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.Tpositive); simpl; try (exists true; auto); intro k; exists (Zpos (k interp_t x)); auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.Tpositive); simpl; try (exists true; auto); intro k; exists (Zneg (k interp_t x)); auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ i])) Typ.TZ); simpl; try (exists true; auto); intro k; exists (- k interp_t x)%Z; auto.
+        (* Binary operators *)
+        intros [ | | | | | | |A] h1 h2; simpl; rewrite andb_true_iff; intros [H1 H2]; destruct (IH h1 H1) as [x Hx]; destruct (IH h2 H2) as [y Hy]; rewrite Hx, Hy; simpl.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x + k2 interp_t y)%Z; auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x - k2 interp_t y)%Z; auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ); simpl; try (exists true; auto); intro k2; exists (k1 interp_t x * k2 interp_t y)%Z; auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x <? k2 interp_t y); auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x <=? k2 interp_t y); auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >=? k2 interp_t y); auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) Typ.TZ); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) Typ.TZ) as [k2| ]; simpl; try (exists true; reflexivity); exists (k1 interp_t x >? k2 interp_t y); auto.
+        case (Typ.cast (v_type Typ.type interp_t (a .[ h1])) A); simpl; try (exists true; auto); intro k1; case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) A) as [k2| ]; simpl; try (exists true; reflexivity); exists (Typ.i_eqb t_i A (k1 interp_t x) (k2 interp_t y)); auto.
+        (* N-ary operators *)
+        intros [A] l; assert (forall acc, List.forallb (fun h0 : int => h0 < h) l = true -> exists v, match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end = Bval (v_type Typ.type interp_t match compute_interp (get a) A acc l with | Some l0 => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l0)) | None => bvtrue end) v); auto; induction l as [ |i l IHl]; simpl.
+        intros acc _; exists (distinct (Typ.i_eqb t_i A) (rev acc)); auto.
+        intro acc; rewrite andb_true_iff; intros [H1 H2]; destruct (IH _ H1) as [va Hva]; rewrite Hva; simpl; case (Typ.cast (v_type Typ.type interp_t (a .[ i])) A); simpl; try (exists true; auto); intro k; destruct (IHl (k interp_t va :: acc) H2) as [vb Hvb]; exists vb; auto.
+        (* Application *)
+        intros i l H; apply (check_aux_interp_aux_lt_aux a h IH l H (t_func.[i])).
+      Qed.
+
+      Lemma check_aux_interp_hatom_lt : forall h, h < length t_atom ->
+        exists v, t_interp.[h] = Bval (get_type h) v.
+      Proof.
+        set (P' i t := length t = length t_atom ->
+          forall j, j < i ->
+            exists v, t.[j] = Bval (v_type Typ.type interp_t (t.[j])) v).
+        assert (P' (length t_atom) t_interp).
+        unfold t_interp;apply foldi_left_Ind;unfold P';intros.
+        rewrite length_set in H1.
+        destruct (Int63Properties.reflect_eqb j i).
+        rewrite e, PArray.get_set_same.
+        apply check_aux_interp_aux_lt; auto.
+        rewrite H1; auto.
+        assert (j < i).
+        assert ([|j|] <> [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial).
+        generalize H2;unfold is_true;rewrite !ltb_spec,
+          (to_Z_add_1 _ _ H);auto with zarith.
+        rewrite get_set_other;auto.
+        elim (ltb_0 _ H0).
+        apply H;apply length_t_interp.
+      Qed.
+
+      Lemma check_aux_interp_hatom : forall h,
+        exists v, t_interp.[h] = Bval (get_type h) v.
+      Proof.
+        intros i;case_eq (i< PArray.length t_atom);intros.
+        apply check_aux_interp_hatom_lt;trivial.
+        unfold get_type'; rewrite !PArray.get_outofbound;trivial.
+        rewrite default_t_interp; simpl; exists (1%positive); auto.
+        rewrite length_t_interp;trivial.
+      Qed.
+
+      Lemma check_aux_interp_aux : forall a t,
+         check_aux get_type a t ->
+         exists v, interp_aux (get t_interp) a = (Bval t v).
+      Proof.
+        intros a t; apply check_aux_interp_aux_aux; apply check_aux_interp_hatom.
+      Qed.
+
+      (* If an atom is not well-typed, its interpretation if bvtrue *)
+
+      Lemma check_aux_interp_aux_contr : forall a,
+        (forall T, check_aux get_type a T = false) ->
+        interp_aux (get t_interp) a = bvtrue.
+      Proof.
+        intros; eapply check_aux_interp_aux_contr_aux; eauto; apply check_aux_interp_hatom.
+      Qed.
+
+    End Interp_get.
+
+
+    Definition get_type t_atom :=
+      get_type' (t_interp t_atom).
+
+    Definition wt t_atom :=
+      let t_interp := t_interp t_atom in
+      let get_type := get_type' t_interp in
+        PArray.forallbi (fun i h => check_aux get_type h (get_type i)) t_atom.
+
+
+    Definition interp_hatom (t_atom : PArray.array atom) :=
+      let t_a := t_interp t_atom in
+      PArray.get t_a.
+
+    Definition interp t_atom := interp_aux (interp_hatom t_atom).
+
+    Definition interp_form_hatom t_atom : hatom -> bool :=
+      let interp := interp_hatom t_atom in
+      fun a => interp_bool (interp a).
+
+  End Typing_Interp.
+
+  Definition check_atom t_atom :=
+    match default t_atom with
+      | Acop CO_xH => wf t_atom
+      | _ => false
+    end.
+
+  Lemma check_atom_correct : forall t_atom, check_atom t_atom ->
+    wf t_atom /\ default t_atom = Acop CO_xH.
+  Proof.
+    intro t_atom; unfold check_atom; case (default t_atom); try discriminate; intro c; case c; auto; discriminate.
+  Qed.
+
+End Atom.