prop
(* -------------------------------------------------------------------- *)
Require Import Bool Arith List.
Local Notation "~~ b" := (negb b) (at level 2).
Local Notation "b1 == b2" := (eqb b1 b2) (at level 70).
(* -------------------------------------------------------------------- *)
(* We are here interested in proving facts about propositional logic. *
* *
* The purpose of this exercice is the proof of the 2 following facts: *
* - 1. natural deduction is correct w.r.t. the interpretation of *
* assertions; *
* - 2. it is decidable to check that an assertion is universally *
* valid. We are going to check that by implementing a sound *
* normalization algorithm for assertions, and then to write, in *
* Coq, a simple decision for the universal validity of the *
* normalized assertions. *)
(* ==================================================================== *)
(* The following datatype describe the syntax of assertions. The *
* constructors for True, the negation and the double implication *
* are not primitive. They are expressed using the other constructions *
* of the logic. *)
Inductive assn : Type :=
| PVar (_ : nat) (* Variable propositionnelle *)
| PFalse (* Faux *)
| PAnd (_ : assn) (_ : assn) (* Conjonction *)
| POr (_ : assn) (_ : assn) (* Disjonction *)
| PImp (_ : assn) (_ : assn). (* Implication *)
Notation PTrue := (PImp PFalse PFalse).
Notation PNot p := (PImp p PFalse).
Notation PIff p q := (PAnd (PImp p q) (PImp q p)).
(* -------------------------------------------------------------------- *)
(* A valuation is simply a function from propositional variables to *
* truth values. *)
Notation valuation := (nat -> bool) (only parsing).
(* -------------------------------------------------------------------- *)
(* Complete the definition of the following function that computes the *
* semantic of an assertion from the given valuation. *)
Fixpoint sem (v : valuation) (p : assn) : bool :=
(* <skip> *)
match p with
| PVar x => v x
| PFalse => false
| PAnd p1 p2 => sem v p1 && sem v p2
| POr p1 p2 => sem v p1 || sem v p2
| PImp p1 p2 => ~~ (sem v p1) || sem v p2
end.
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* We now define the notions of begin satisfiable under a valuation *
* and of being universally valid. *)
Definition sat (v : valuation) (p : assn) :=
sem v p = true.
Definition valid (p : assn) :=
forall v, sat v p.
(* -------------------------------------------------------------------- *)
(* The following inductive predicate defines the notion of judgement *
* in natural deduction. This predicate accepts two arguments: *
* *
* - a list of assertions that stands for the proof context; *
* - the assertion that is proven under this context. *)
Inductive dn : list assn -> assn -> Prop :=
(* Non-structural rules *)
| Ax env p :
In p env -> dn env p
| Absurd env p :
dn (PNot p :: env) PFalse -> dn env p
(* Introduction rules *)
| AndI env p q : dn env p -> dn env q -> dn env (PAnd p q)
| OrIL env p q : dn env p -> dn env (POr p q)
| OrIR env p q : dn env q -> dn env (POr p q)
| ImpI env p q : dn (p :: env) q -> dn env (PImp p q)
(* Elimination rules *)
| FalseE env p : dn env PFalse -> dn env p
| AndEL env p q : dn env (PAnd p q) -> dn env p
| AndER env p q : dn env (PAnd p q) -> dn env q
| OrE env p q r : dn env (POr p q) -> dn (p :: env) r -> dn (q :: env) r -> dn env r
| ImpE env p q : dn env p -> dn env (PImp p q) -> dn env q
.
(* <hide> *)
Hint Constructors dn : prop.
(* </hide> *)
(* -------------------------------------------------------------------- *)
(* We first start to prove that the predicate dn is stable by *
* weakening or permuting the proof context. The following definition *
* defines an ordering over proof contexts. *)
Definition subenv (e1 e2 : list assn) :=
forall q, In q e1 -> In q e2.
(* <hide> *)
Definition subenv_cons (e1 e2 : list assn) (p : assn) :
subenv e1 e2 -> subenv (p :: e1) (p :: e2).
Proof.
intros se q qin; apply in_inv in qin; destruct qin as [eq|h].
+ now rewrite eq; left. + now right; apply se.
Qed.
Hint Resolve subenv_cons : prop.
(* </hide> *)
(* -------------------------------------------------------------------- *)
(* Show that dn is monotone from subenv *)
Lemma subenv_dn (e1 e2 : list assn) (p : assn) :
subenv e1 e2 -> dn e1 p -> dn e2 p.
Proof.
(* <skip> *)
intros sube dn1; revert e2 sube; induction dn1; intros; eauto 4 with prop.
+ now apply OrE with p q; eauto with prop.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* We now prove the correctness of dn. Prove the following lemma, *
* by induction on dn env p. *)
Lemma correctness (env : list assn) (p : assn) :
dn env p -> forall v, (forall q, In q env -> sat v q) -> sat v p.
Proof.
(* <skip> *)
unfold sat; induction 1; simpl; intros v sate.
+ now apply sate.
+ case_eq (sem v p); [trivial | intros sp; apply (IHdn v)].
intros q qine; apply in_inv in qine; case qine; auto.
now intros eq; rewrite <- eq; simpl; rewrite sp.
+ now apply andb_true_iff; split; [apply IHdn1 | apply IHdn2].
+ now apply orb_true_iff; auto.
+ now apply orb_true_iff; auto.
+ apply orb_true_iff; case_eq (sem v p); [intros semvp; right|tauto].
apply IHdn; intros r rinXe; apply in_inv in rinXe.
now case rinXe; [intros eq; rewrite <- eq|auto].
+ now case (sem v p); [|apply (IHdn v)].
+ now assert (h := IHdn _ sate); simpl in h; apply andb_true_iff in h.
+ now assert (h := IHdn _ sate); simpl in h; apply andb_true_iff in h.
+ assert (h := IHdn1 _ sate); simpl in h; apply orb_true_iff in h.
case h as [eq|eq]; [apply IHdn2| apply IHdn3]; intros t tine;
now apply in_inv in tine; case tine; intros; subst; auto.
+ now generalize (IHdn2 _ sate); simpl; rewrite (IHdn1 _ sate).
(* </skip> *)
Qed.
(* ==================================================================== *)
(* We are now interested in deciding if a given assertion is *
* universally valid or not. For that, we first normalize the *
* assertions, obtaining an expression built from boolean constants, *
* propositionnal variables and if-then-else statements whose *
* condition is a propositional variables. *)
(* -------------------------------------------------------------------- *)
(* We start by defining an intermediate datatype that describe the *
* syntax of normalized assertions, except for the side conditions *
* of the if-then-else expressions that are still unconstrained. *)
Inductive ifassn : Type :=
| PIVar (_ : nat) (* variable propositionnelle *)
| PIConst (_ : bool) (* constante true / false *)
| PIIf (_ : ifassn) (_ : ifassn) (_ : ifassn). (* if-then-else *)
(* -------------------------------------------------------------------- *)
(* Define the semantic of the assertions of type ifassn. *)
Fixpoint ifsem (v : valuation) (p : ifassn) : bool :=
(* <skip> *)
match p with
| PIVar x => v x
| PIConst b => b
| PIIf c t f => if ifsem v c then ifsem v t else ifsem v f
end.
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* Write the normalization functions from assertions of type assn to *
* assertions of type ifassn. *)
Fixpoint ifassn_of_assn (p : assn) :=
(* <skip> *)
match p with
| PVar x => PIVar x
| PFalse => PIConst false
| PAnd p1 p2 => PIIf (ifassn_of_assn p1) (ifassn_of_assn p2) (PIConst false)
| POr p1 p2 => PIIf (ifassn_of_assn p1) (PIConst true) (ifassn_of_assn p2)
| PImp p1 p2 => PIIf (ifassn_of_assn p1) (ifassn_of_assn p2) (PIConst true)
end.
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* Show that your normalization function is correct w.r.t. ifsem. *)
Lemma ifassn_correct (v : valuation) (p : assn) :
sem v p = ifsem v (ifassn_of_assn p).
Proof.
(* <skip> *)
elim p; simpl; auto; intros q ihq r ihr;
now rewrite <- ihq, <- ihr; case (sem v q).
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* We now define the syntax of normalized assertions. We see that the *
* conditions of the if-then-else expressions are now enforced to be *
* propositional variables. *)
Inductive nifassn : Type :=
| PNIVar (_ : nat)
| PNIConst (_ : bool)
| PNIIf (_ : nat) (_ : nifassn) (_ : nifassn).
(* -------------------------------------------------------------------- *)
(* Define the semantic of the assertions of type nifassn. *)
Fixpoint nifsem (v : valuation) (p : nifassn) : bool :=
(* <skip> *)
match p with
| PNIVar x => v x
| PNIConst b => b
| PNIIf x t f => if v x then nifsem v t else nifsem v f
end.
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* We define below the normalization function for assertions of type *
* ifassn, obtaining assertions of type nifassn. *)
Fixpoint normif (c t f : nifassn) {struct c} :=
match c with
| PNIVar x => PNIIf x t f
| PNIConst true => t
| PNIConst false => f
| PNIIf c' t' f' => PNIIf c' (normif t' t f) (normif f' t f)
end.
Fixpoint norm (p : ifassn) : nifassn :=
match p with
| PIVar x => PNIVar x
| PIConst b => PNIConst b
| PIIf c t f => normif (norm c) (norm t) (norm f)
end.
(* -------------------------------------------------------------------- *)
(* Show that the normalization functions are correct w.r.t. nifsem. *)
Lemma normif_correct (v : valuation) (c t f : nifassn) :
nifsem v (normif c t f) = if nifsem v c then nifsem v t else nifsem v f.
Proof. elim c; simpl; auto.
(* <skip> *)
+ now intros b; case b.
+ now intros x t' iht' f' ihf'; case (v x); [rewrite iht' | rewrite ihf'].
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
Lemma norm_correct (v : valuation) (p : ifassn) : nifsem v (norm p) = ifsem v p.
Proof.
(* <skip> *)
elim p; simpl; auto; intros c ihc t iht f ihf.
now rewrite <- ihc, normif_correct, iht, ihf.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* Finally, we provide a procedure that decides if a normalized *
* assertion is universally valid w.r.t. nifasm. *)
Definition xt (v : nat -> option bool) (x : nat) (b : bool) :=
fun y => if beq_nat x y then Some b else v y.
Fixpoint nifassn_tauto_r (v : nat -> option bool) (p : nifassn) :=
match p with
| PNIVar x => match v x with Some true => true | _ => false end
| PNIConst b => b
| PNIIf x t f =>
match v x with
| Some true => nifassn_tauto_r v t
| Some false => nifassn_tauto_r v f
| None =>
nifassn_tauto_r (xt v x true ) t
&& nifassn_tauto_r (xt v x false) f
end
end.
Definition nifassn_tauto p := nifassn_tauto_r (fun _ => None) p.
(* -------------------------------------------------------------------- *)
(* Show the correctness of the procedure... *)
Lemma nifassn_tauto_r_correct (xv : nat -> option bool) (p : nifassn) :
nifassn_tauto_r xv p = true
-> forall v, (forall x b, xv x = Some b -> v x = b)
-> nifsem v p = true.
Proof.
(* <skip> *)
revert xv; elim p; simpl; auto.
+ intros x xv Vxv v hv; apply hv; revert Vxv.
now case (xv x) as [b|]; [case b|].
+ intros x t iht f ihf xv Vxv v hv; revert Vxv hv.
case_eq (xv x); [intros b; case b; intros xvE h hv|].
* now rewrite (hv _ _ xvE); apply (iht xv).
* now rewrite (hv _ _ xvE); apply (ihf xv).
* intros xvE h hv; apply andb_true_iff in h; case h as [h1 h2].
case_eq (v x); intros vxE; [apply (iht _ h1) | apply (ihf _ h2)].
- intros y b; unfold xt; case_eq (Nat.eqb x y); intros heq.
++ apply beq_nat_true_iff in heq; rewrite <- heq.
now intros bE; injection bE; clear bE; intros bE; subst b.
++ now apply hv.
- intros y b; unfold xt; case_eq (Nat.eqb x y); intros heq.
++ apply beq_nat_true_iff in heq; rewrite <- heq.
now intros bE; injection bE; clear bE; intros bE; subst b.
++ now apply hv.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
Lemma nifassn_tauto_correct (p : nifassn) :
nifassn_tauto p = true -> forall v, nifsem v p = true.
Proof.
(* <skip> *)
now intros h v; assert (h' := nifassn_tauto_r_correct _ _ h v); apply h'.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* ...and its completness. *)
Lemma nifassn_tauto_r_complete (xv : nat -> option bool) (p : nifassn) :
nifassn_tauto_r xv p = false
-> exists v, (forall x b, xv x = Some b -> v x = b) /\ nifsem v p = false.
Proof.
(* <skip> *)
revert xv; elim p; simpl.
+ intros x xv; case_eq (xv x); [intros []; [easy|intros xvE _]|intros xvE _].
- exists (fun x => match xv x with Some b => b | _ => false end).
now rewrite xvE; split; [intros y n xvyE; rewrite xvyE|easy].
- exists (fun x => match xv x with Some b => b | _ => false end).
now rewrite xvE; split; [intros y b xvyE; rewrite xvyE|easy].
+ intros b xv bE; subst b.
exists (fun x => match xv x with Some b => b | _ => false end).
now split; [intros x b xvE|easy]; rewrite xvE.
+ intros x t iht f ihf xv; case_eq (xv x); [intros b|].
- case b; intros xvE h; [apply iht in h|apply ihf in h].
* case h; intros v [h1 h2]; exists v; split; [easy|].
now rewrite (h1 _ _ xvE).
* case h; intros v [h1 h2]; exists v; split; [easy|].
now rewrite (h1 _ _ xvE).
- intros xvE h; apply andb_false_iff in h; case h; clear h; intros h.
* case (iht _ h); intros v [h1 h2]; exists v; split.
++ intros y b; case_eq (x =? y); intros xy.
-- now apply beq_nat_true_iff in xy; rewrite <- xy, xvE.
-- intros xvyE; generalize (h1 y b); unfold xt.
now rewrite xy; intros h'; apply h'.
++ now rewrite (h1 x true); [|unfold xt; rewrite <- beq_nat_refl].
* case (ihf _ h); intros v [h1 h2]; exists v; split.
++ intros y b; case_eq (x =? y); intros xy.
-- now apply beq_nat_true_iff in xy; rewrite <- xy, xvE.
-- intros xvyE; generalize (h1 y b); unfold xt.
now rewrite xy; intros h'; apply h'.
++ now rewrite (h1 x false); [|unfold xt; rewrite <- beq_nat_refl].
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
Lemma nifassn_tauto_complete (p : nifassn) :
nifassn_tauto p = false -> exists v, nifsem v p = false.
Proof.
(* <skip> *)
intros h; case (nifassn_tauto_r_complete _ _ h).
now intros v [_ hv]; exists v.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* From this, define a decision procedure for the univdesal validity *
* and non-normalized assertions. *)
Definition is_tautology (p : assn) : bool :=
(* <skip> *)
nifassn_tauto (norm (ifassn_of_assn p)).
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* Show the correctness of the procedure... *)
Lemma is_tautology_correct (p : assn) : is_tautology p = true -> valid p.
Proof.
(* <skip> *)
intros h v; generalize (nifassn_tauto_correct _ h v).
now rewrite norm_correct, <- ifassn_correct.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* ...and its completness. *)
Lemma is_tautology_complete (p : assn) :
is_tautology p = false -> exists v, sem v p = false.
Proof.
(* <skip> *)
unfold is_tautology.
case_eq (nifassn_tauto (norm (ifassn_of_assn p))); [easy|].
intros h; case (nifassn_tauto_complete _ h); intros v hv _.
now rewrite <- hv; exists v; rewrite norm_correct, <- ifassn_correct.
(* </skip> *)
Qed.
Require Import Bool Arith List.
Local Notation "~~ b" := (negb b) (at level 2).
Local Notation "b1 == b2" := (eqb b1 b2) (at level 70).
(* -------------------------------------------------------------------- *)
(* We are here interested in proving facts about propositional logic. *
* *
* The purpose of this exercice is the proof of the 2 following facts: *
* - 1. natural deduction is correct w.r.t. the interpretation of *
* assertions; *
* - 2. it is decidable to check that an assertion is universally *
* valid. We are going to check that by implementing a sound *
* normalization algorithm for assertions, and then to write, in *
* Coq, a simple decision for the universal validity of the *
* normalized assertions. *)
(* ==================================================================== *)
(* The following datatype describe the syntax of assertions. The *
* constructors for True, the negation and the double implication *
* are not primitive. They are expressed using the other constructions *
* of the logic. *)
Inductive assn : Type :=
| PVar (_ : nat) (* Variable propositionnelle *)
| PFalse (* Faux *)
| PAnd (_ : assn) (_ : assn) (* Conjonction *)
| POr (_ : assn) (_ : assn) (* Disjonction *)
| PImp (_ : assn) (_ : assn). (* Implication *)
Notation PTrue := (PImp PFalse PFalse).
Notation PNot p := (PImp p PFalse).
Notation PIff p q := (PAnd (PImp p q) (PImp q p)).
(* -------------------------------------------------------------------- *)
(* A valuation is simply a function from propositional variables to *
* truth values. *)
Notation valuation := (nat -> bool) (only parsing).
(* -------------------------------------------------------------------- *)
(* Complete the definition of the following function that computes the *
* semantic of an assertion from the given valuation. *)
Fixpoint sem (v : valuation) (p : assn) : bool :=
(* <skip> *)
match p with
| PVar x => v x
| PFalse => false
| PAnd p1 p2 => sem v p1 && sem v p2
| POr p1 p2 => sem v p1 || sem v p2
| PImp p1 p2 => ~~ (sem v p1) || sem v p2
end.
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* We now define the notions of begin satisfiable under a valuation *
* and of being universally valid. *)
Definition sat (v : valuation) (p : assn) :=
sem v p = true.
Definition valid (p : assn) :=
forall v, sat v p.
(* -------------------------------------------------------------------- *)
(* The following inductive predicate defines the notion of judgement *
* in natural deduction. This predicate accepts two arguments: *
* *
* - a list of assertions that stands for the proof context; *
* - the assertion that is proven under this context. *)
Inductive dn : list assn -> assn -> Prop :=
(* Non-structural rules *)
| Ax env p :
In p env -> dn env p
| Absurd env p :
dn (PNot p :: env) PFalse -> dn env p
(* Introduction rules *)
| AndI env p q : dn env p -> dn env q -> dn env (PAnd p q)
| OrIL env p q : dn env p -> dn env (POr p q)
| OrIR env p q : dn env q -> dn env (POr p q)
| ImpI env p q : dn (p :: env) q -> dn env (PImp p q)
(* Elimination rules *)
| FalseE env p : dn env PFalse -> dn env p
| AndEL env p q : dn env (PAnd p q) -> dn env p
| AndER env p q : dn env (PAnd p q) -> dn env q
| OrE env p q r : dn env (POr p q) -> dn (p :: env) r -> dn (q :: env) r -> dn env r
| ImpE env p q : dn env p -> dn env (PImp p q) -> dn env q
.
(* <hide> *)
Hint Constructors dn : prop.
(* </hide> *)
(* -------------------------------------------------------------------- *)
(* We first start to prove that the predicate dn is stable by *
* weakening or permuting the proof context. The following definition *
* defines an ordering over proof contexts. *)
Definition subenv (e1 e2 : list assn) :=
forall q, In q e1 -> In q e2.
(* <hide> *)
Definition subenv_cons (e1 e2 : list assn) (p : assn) :
subenv e1 e2 -> subenv (p :: e1) (p :: e2).
Proof.
intros se q qin; apply in_inv in qin; destruct qin as [eq|h].
+ now rewrite eq; left. + now right; apply se.
Qed.
Hint Resolve subenv_cons : prop.
(* </hide> *)
(* -------------------------------------------------------------------- *)
(* Show that dn is monotone from subenv *)
Lemma subenv_dn (e1 e2 : list assn) (p : assn) :
subenv e1 e2 -> dn e1 p -> dn e2 p.
Proof.
(* <skip> *)
intros sube dn1; revert e2 sube; induction dn1; intros; eauto 4 with prop.
+ now apply OrE with p q; eauto with prop.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* We now prove the correctness of dn. Prove the following lemma, *
* by induction on dn env p. *)
Lemma correctness (env : list assn) (p : assn) :
dn env p -> forall v, (forall q, In q env -> sat v q) -> sat v p.
Proof.
(* <skip> *)
unfold sat; induction 1; simpl; intros v sate.
+ now apply sate.
+ case_eq (sem v p); [trivial | intros sp; apply (IHdn v)].
intros q qine; apply in_inv in qine; case qine; auto.
now intros eq; rewrite <- eq; simpl; rewrite sp.
+ now apply andb_true_iff; split; [apply IHdn1 | apply IHdn2].
+ now apply orb_true_iff; auto.
+ now apply orb_true_iff; auto.
+ apply orb_true_iff; case_eq (sem v p); [intros semvp; right|tauto].
apply IHdn; intros r rinXe; apply in_inv in rinXe.
now case rinXe; [intros eq; rewrite <- eq|auto].
+ now case (sem v p); [|apply (IHdn v)].
+ now assert (h := IHdn _ sate); simpl in h; apply andb_true_iff in h.
+ now assert (h := IHdn _ sate); simpl in h; apply andb_true_iff in h.
+ assert (h := IHdn1 _ sate); simpl in h; apply orb_true_iff in h.
case h as [eq|eq]; [apply IHdn2| apply IHdn3]; intros t tine;
now apply in_inv in tine; case tine; intros; subst; auto.
+ now generalize (IHdn2 _ sate); simpl; rewrite (IHdn1 _ sate).
(* </skip> *)
Qed.
(* ==================================================================== *)
(* We are now interested in deciding if a given assertion is *
* universally valid or not. For that, we first normalize the *
* assertions, obtaining an expression built from boolean constants, *
* propositionnal variables and if-then-else statements whose *
* condition is a propositional variables. *)
(* -------------------------------------------------------------------- *)
(* We start by defining an intermediate datatype that describe the *
* syntax of normalized assertions, except for the side conditions *
* of the if-then-else expressions that are still unconstrained. *)
Inductive ifassn : Type :=
| PIVar (_ : nat) (* variable propositionnelle *)
| PIConst (_ : bool) (* constante true / false *)
| PIIf (_ : ifassn) (_ : ifassn) (_ : ifassn). (* if-then-else *)
(* -------------------------------------------------------------------- *)
(* Define the semantic of the assertions of type ifassn. *)
Fixpoint ifsem (v : valuation) (p : ifassn) : bool :=
(* <skip> *)
match p with
| PIVar x => v x
| PIConst b => b
| PIIf c t f => if ifsem v c then ifsem v t else ifsem v f
end.
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* Write the normalization functions from assertions of type assn to *
* assertions of type ifassn. *)
Fixpoint ifassn_of_assn (p : assn) :=
(* <skip> *)
match p with
| PVar x => PIVar x
| PFalse => PIConst false
| PAnd p1 p2 => PIIf (ifassn_of_assn p1) (ifassn_of_assn p2) (PIConst false)
| POr p1 p2 => PIIf (ifassn_of_assn p1) (PIConst true) (ifassn_of_assn p2)
| PImp p1 p2 => PIIf (ifassn_of_assn p1) (ifassn_of_assn p2) (PIConst true)
end.
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* Show that your normalization function is correct w.r.t. ifsem. *)
Lemma ifassn_correct (v : valuation) (p : assn) :
sem v p = ifsem v (ifassn_of_assn p).
Proof.
(* <skip> *)
elim p; simpl; auto; intros q ihq r ihr;
now rewrite <- ihq, <- ihr; case (sem v q).
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* We now define the syntax of normalized assertions. We see that the *
* conditions of the if-then-else expressions are now enforced to be *
* propositional variables. *)
Inductive nifassn : Type :=
| PNIVar (_ : nat)
| PNIConst (_ : bool)
| PNIIf (_ : nat) (_ : nifassn) (_ : nifassn).
(* -------------------------------------------------------------------- *)
(* Define the semantic of the assertions of type nifassn. *)
Fixpoint nifsem (v : valuation) (p : nifassn) : bool :=
(* <skip> *)
match p with
| PNIVar x => v x
| PNIConst b => b
| PNIIf x t f => if v x then nifsem v t else nifsem v f
end.
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* We define below the normalization function for assertions of type *
* ifassn, obtaining assertions of type nifassn. *)
Fixpoint normif (c t f : nifassn) {struct c} :=
match c with
| PNIVar x => PNIIf x t f
| PNIConst true => t
| PNIConst false => f
| PNIIf c' t' f' => PNIIf c' (normif t' t f) (normif f' t f)
end.
Fixpoint norm (p : ifassn) : nifassn :=
match p with
| PIVar x => PNIVar x
| PIConst b => PNIConst b
| PIIf c t f => normif (norm c) (norm t) (norm f)
end.
(* -------------------------------------------------------------------- *)
(* Show that the normalization functions are correct w.r.t. nifsem. *)
Lemma normif_correct (v : valuation) (c t f : nifassn) :
nifsem v (normif c t f) = if nifsem v c then nifsem v t else nifsem v f.
Proof. elim c; simpl; auto.
(* <skip> *)
+ now intros b; case b.
+ now intros x t' iht' f' ihf'; case (v x); [rewrite iht' | rewrite ihf'].
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
Lemma norm_correct (v : valuation) (p : ifassn) : nifsem v (norm p) = ifsem v p.
Proof.
(* <skip> *)
elim p; simpl; auto; intros c ihc t iht f ihf.
now rewrite <- ihc, normif_correct, iht, ihf.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* Finally, we provide a procedure that decides if a normalized *
* assertion is universally valid w.r.t. nifasm. *)
Definition xt (v : nat -> option bool) (x : nat) (b : bool) :=
fun y => if beq_nat x y then Some b else v y.
Fixpoint nifassn_tauto_r (v : nat -> option bool) (p : nifassn) :=
match p with
| PNIVar x => match v x with Some true => true | _ => false end
| PNIConst b => b
| PNIIf x t f =>
match v x with
| Some true => nifassn_tauto_r v t
| Some false => nifassn_tauto_r v f
| None =>
nifassn_tauto_r (xt v x true ) t
&& nifassn_tauto_r (xt v x false) f
end
end.
Definition nifassn_tauto p := nifassn_tauto_r (fun _ => None) p.
(* -------------------------------------------------------------------- *)
(* Show the correctness of the procedure... *)
Lemma nifassn_tauto_r_correct (xv : nat -> option bool) (p : nifassn) :
nifassn_tauto_r xv p = true
-> forall v, (forall x b, xv x = Some b -> v x = b)
-> nifsem v p = true.
Proof.
(* <skip> *)
revert xv; elim p; simpl; auto.
+ intros x xv Vxv v hv; apply hv; revert Vxv.
now case (xv x) as [b|]; [case b|].
+ intros x t iht f ihf xv Vxv v hv; revert Vxv hv.
case_eq (xv x); [intros b; case b; intros xvE h hv|].
* now rewrite (hv _ _ xvE); apply (iht xv).
* now rewrite (hv _ _ xvE); apply (ihf xv).
* intros xvE h hv; apply andb_true_iff in h; case h as [h1 h2].
case_eq (v x); intros vxE; [apply (iht _ h1) | apply (ihf _ h2)].
- intros y b; unfold xt; case_eq (Nat.eqb x y); intros heq.
++ apply beq_nat_true_iff in heq; rewrite <- heq.
now intros bE; injection bE; clear bE; intros bE; subst b.
++ now apply hv.
- intros y b; unfold xt; case_eq (Nat.eqb x y); intros heq.
++ apply beq_nat_true_iff in heq; rewrite <- heq.
now intros bE; injection bE; clear bE; intros bE; subst b.
++ now apply hv.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
Lemma nifassn_tauto_correct (p : nifassn) :
nifassn_tauto p = true -> forall v, nifsem v p = true.
Proof.
(* <skip> *)
now intros h v; assert (h' := nifassn_tauto_r_correct _ _ h v); apply h'.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* ...and its completness. *)
Lemma nifassn_tauto_r_complete (xv : nat -> option bool) (p : nifassn) :
nifassn_tauto_r xv p = false
-> exists v, (forall x b, xv x = Some b -> v x = b) /\ nifsem v p = false.
Proof.
(* <skip> *)
revert xv; elim p; simpl.
+ intros x xv; case_eq (xv x); [intros []; [easy|intros xvE _]|intros xvE _].
- exists (fun x => match xv x with Some b => b | _ => false end).
now rewrite xvE; split; [intros y n xvyE; rewrite xvyE|easy].
- exists (fun x => match xv x with Some b => b | _ => false end).
now rewrite xvE; split; [intros y b xvyE; rewrite xvyE|easy].
+ intros b xv bE; subst b.
exists (fun x => match xv x with Some b => b | _ => false end).
now split; [intros x b xvE|easy]; rewrite xvE.
+ intros x t iht f ihf xv; case_eq (xv x); [intros b|].
- case b; intros xvE h; [apply iht in h|apply ihf in h].
* case h; intros v [h1 h2]; exists v; split; [easy|].
now rewrite (h1 _ _ xvE).
* case h; intros v [h1 h2]; exists v; split; [easy|].
now rewrite (h1 _ _ xvE).
- intros xvE h; apply andb_false_iff in h; case h; clear h; intros h.
* case (iht _ h); intros v [h1 h2]; exists v; split.
++ intros y b; case_eq (x =? y); intros xy.
-- now apply beq_nat_true_iff in xy; rewrite <- xy, xvE.
-- intros xvyE; generalize (h1 y b); unfold xt.
now rewrite xy; intros h'; apply h'.
++ now rewrite (h1 x true); [|unfold xt; rewrite <- beq_nat_refl].
* case (ihf _ h); intros v [h1 h2]; exists v; split.
++ intros y b; case_eq (x =? y); intros xy.
-- now apply beq_nat_true_iff in xy; rewrite <- xy, xvE.
-- intros xvyE; generalize (h1 y b); unfold xt.
now rewrite xy; intros h'; apply h'.
++ now rewrite (h1 x false); [|unfold xt; rewrite <- beq_nat_refl].
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
Lemma nifassn_tauto_complete (p : nifassn) :
nifassn_tauto p = false -> exists v, nifsem v p = false.
Proof.
(* <skip> *)
intros h; case (nifassn_tauto_r_complete _ _ h).
now intros v [_ hv]; exists v.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* From this, define a decision procedure for the univdesal validity *
* and non-normalized assertions. *)
Definition is_tautology (p : assn) : bool :=
(* <skip> *)
nifassn_tauto (norm (ifassn_of_assn p)).
(* </skip> *)
(* -------------------------------------------------------------------- *)
(* Show the correctness of the procedure... *)
Lemma is_tautology_correct (p : assn) : is_tautology p = true -> valid p.
Proof.
(* <skip> *)
intros h v; generalize (nifassn_tauto_correct _ h v).
now rewrite norm_correct, <- ifassn_correct.
(* </skip> *)
Qed.
(* -------------------------------------------------------------------- *)
(* ...and its completness. *)
Lemma is_tautology_complete (p : assn) :
is_tautology p = false -> exists v, sem v p = false.
Proof.
(* <skip> *)
unfold is_tautology.
case_eq (nifassn_tauto (norm (ifassn_of_assn p))); [easy|].
intros h; case (nifassn_tauto_complete _ h); intros v hv _.
now rewrite <- hv; exists v; rewrite norm_correct, <- ifassn_correct.
(* </skip> *)
Qed.