Set Implicit Arguments.

Require Import BDT Formula.

(** * Ecrire une fonction qui transforme une formule en un BDT équivalent *)
Print form.

Fixpoint form2bdt (f:form) : bdt := 
   match f with 
     Atom a => (* compléter *)
   | Var x => 
   | Neg p => 
   | Bin o p q => 
   end.

(** Tester la fonction *)
Eval compute in form2bdt P1.
Eval compute in form2bdt P2.

(** Prouver que la transformation form2bdt préserve la sémantique des formules *)

Lemma form2bdt_corr : forall I f, interp I f = interpt I (form2bdt f).
Proof.
(* compléter *)
Qed.

(** A quelle condition sur i j n m a-t-on ordered n i t -> ordered m j t ?
    faire la preuve correspondante *)

Lemma ordered_incl : forall n i t, ordered n i t -> 
      forall m j, (* compléter *) -> ordered m j t.
Proof.
(* compléter *)
Qed.

(** Définir une fonction qui renvoie le maximum des variables 
   rencontrées dans une formule propositionnelle +1 (0 si pas de variable) 
   on pourra utiliser la fonction max *)

Fixpoint maxvar (f:form) : nat := 
   match f with 
     Atom a => 
   | Var x => 
   | Neg p => 
   | Bin o p q => 
   end.

(** Prouver que le résultat de form2bdt donne un arbre ordonné entre 0 et maxvar *)

Lemma form2bdt_ord : forall f, ordered (maxvar f) 0 (form2bdt f).
Proof.
(* compléter *)
Qed.

(** * Tester qu'un BDT (ordonné) est une tautologie *)
(* Ecrire une fonction booléenne qui teste si un BDT correspond à une tautologie *)

Fixpoint istauto (t:bdt) : bool := 
   match t with Atomt a =>  (* compléter *) | IFt x l r =>  (* compléter *) end. 

(** Enoncer et prouver la correction de ce test, on pourra distinguer 
    le cas où le test est positif et le cas où le test est négatif *)

Lemma istauto_true_corr : forall (t:bdt), istauto t = true 
      -> (* compléter *).
Proof.

Save.

Lemma istauto_false_corr : forall (t:bdt), 
         istauto t = false -> (* compléter *).
Proof.

Qed.