Hello,
I am reading book by Adam Chlipala.
http://adam.chlipala.net/cpdt/cpdt.pdf
In chapter Programming with dependent types → Subset types and variations, I faced this exercise:
Implement the DPLL satisfiability decision procedure for boolean formulas in conjunctive normal form, with a dependent type that guarantees its correctness.
An example of a reasonable type for this function would be
∀ f : formula, {truth : tvals  formulaTrue truth f } + {∀ truth, ¬ formulaTrue truth f }.
Implement at least “the basic backtracking algorithm” as defined here:
It might also be instructive to implement the unit propagation and pure literal elimination optimizations described there or some other optimizations that have been used
in modern SAT solvers
Exercise can be found here:
http://adam.chlipala.net/cpdt/ex/exercises.pdf
Definition var := nat % type.
Definition partial_map := var > option bool.
Definition empty : partial_map :=
(fun _ => None).
Definition tvals := partial_map.
Inductive formula : Set :=
 Var : var > formula
 Not : var > formula
 Disj : formula > formula > formula
 Conj : formula > formula > formula.
To keep conjunctive normal form this definition of formula below would be better, I tried both, but in current version I am using first one.
Inductive literal : Set :=
 Var : var > literal
 Not : var > literal
 Disj : literal > literal > literal.
Inductive formula : Set :=
 Lit : literal > formula
 Conj : formula > formula > formula.
Definition nodup_var := nodup eq_nat_dec.
(* To calculate all vars in formula. *)
Fixpoint vars_in_formula f : list var :=
match f with
 Var v => v :: nil
 Not v => v :: nil
 Disj f1 f2 => nodup_var (vars_in_formula f1 ++ vars_in_formula f2)
 Conj f1 f2 => nodup_var (vars_in_formula f1 ++ vars_in_formula f2)
end.
I can solve task, using maybe type. This is solution:
Inductive maybe (A : Set) (P : A > Prop) : Set :=
 Unknown : maybe P
 Found : forall x : A, P x > maybe P.
(* we can define some new notations for convenient usage of type maybe. *)
Notation "{{ x  P }}" := (maybe (fun x => P)).
Notation "??" := (Unknown _ ).
Notation "[ x ]" := (Found _ x _).
Fixpoint evalFormula f (map : tvals) {struct f} : option bool :=
match f with
 Var v => map v
 Not v => match map v with
 Some true => Some false
 Some false => Some true
 None => None (* вовсе не определена функция на мапе? надо бы все None *)
end
 Disj f1 f2 => match (evalFormula f1 map) with
 Some true => match (evalFormula f2 map) with
 Some true => Some true
 Some false => Some true
 None => None
end
 Some false => match (evalFormula f2 map) with
 Some true => Some true
 Some false => Some false
 None => None
end
 None => None (* вовсе не определена функция на мапе? надо бы все None *)
end
 Conj f1 f2 => match (evalFormula f1 map) with
 Some true => match evalFormula f2 map with
 Some true => Some true
 Some false => Some false
 None => None
end
 Some false => match evalFormula f2 map with (* чтоб решить что возвращать, None и *)
 Some true => Some false
 Some false => Some false
 None => None
end
 None => None
end
end.
Definition checkVars : forall (ls : list var) (f : formula) (map : tvals), {{ map'  evalFormula f map' = Some true }}.
refine (fix F (ls : list var) (f : formula) (map : tvals) : {{ map'  evalFormula f map' = Some true }} :=
match ls with
 nil => _
 x :: xs => match F xs f (x !> Some true; map) with
 ?? => F xs f (x !> Some false; map)
 res => res
end
end).
destruct (evalFormula f map) eqn:E.
 destruct b.
+ eapply (Found _ map E).
+ apply ??.
 apply ??.
Defined.
Definition f := (Disj (Var 1) (Disj (Var 2) (Not 3))).
Eval simpl in checkVars (nodup_var (vars_in_formula f)) f empty.
Definition f1 := (Conj (Var 1) (Not 1)).
Eval simpl in checkVars ((vars_in_formula f1)) f1 empty.
See? It works and even works correctly, I can detect if formula is not satisfiable or not, and find tvals (map) which satisfies the formula.
But, Adam Chlipala in his exercise asked to prove a strengthened statement :
∀ f : formula, {truth : tvals  formulaTrue truth f } + {∀ truth, ¬ formulaTrue truth f }.
He asked to prove : ∀ truth, ¬ formulaTrue truth f.
I am not able to do it, and asking for advice.
I tried several approaches:
Approach 1

 create all possible tvals (partial maps), 2. try each one, 3. if no map that satisfies formula found, prove that forall maps formula is unsutisfiable (I failed to do this one),
and this is obviously not a good sulution, cos if we create list of all possible maps, we will not be able to implement optimizations : unit propagation and pure literal elimi
nation.
 create all possible tvals (partial maps), 2. try each one, 3. if no map that satisfies formula found, prove that forall maps formula is unsutisfiable (I failed to do this one),
Approach 2
 use fuel : create an Axiom that (all possible permutations equals factorial (amount_of_vars_in_formula)), so if all maps checked and we run out of fuel  formula is unsatisfiable forall tvals.
is this a cheating?
Approach 3
 create a lot of dependent types (formula_maps, formula_vars, …). Failed. Couldn’t prove {∀ truth, ¬ formulaTrue truth f }
Below is version with fuel and dependent types (I am working on it now).
Inductive formula_List_Vars : list var > formula > Set :=
 FVars_Var : forall v ls, In_var_ls' v ls = true > NoDup ls > formula_List_Vars ls (Var v)
 FVars_Not : forall v ls, In_var_ls' v ls = true > NoDup ls > formula_List_Vars ls (Not v)
 FVars_Disj : forall f1 f2 ls1 ls2, NoDup ls1 > NoDup ls2 >
formula_List_Vars ls1 f1>
formula_List_Vars ls2 f2 >
formula_List_Vars (nodup_var (ls1 ++ ls2)) (Disj f1 f2)
 FVars_Conj : forall f1 f2 ls1 ls2, NoDup ls1 > NoDup ls2 >
formula_List_Vars ls1 f1 >
formula_List_Vars ls2 f2 >
formula_List_Vars (nodup_var (ls1 ++ ls2)) (Conj f1 f2).
Inductive formula_map : tvals > formula > Prop :=
 FM_Var : forall map var b, map var = Some b >
formula_map map (Var var)
 FM_Not : forall map var b, map var = Some b >
formula_map map (Not var)
 FM_Disj : forall f1 f2 map, formula_map map f1 >
formula_map map f2 >
formula_map map (Disj f1 f2)
 FM_Conj : forall f1 f2 map, formula_map map f1 >
formula_map map f2 >
formula_map map (Conj f1 f2).
Inductive formulaTrue : tvals > formula > Prop :=
 TVar : forall tv var, tv var = Some true > formula_map tv (Var var) > formulaTrue tv (Var var)
 TNot : forall tv var, tv var = Some false > formula_map tv (Not var) > formulaTrue tv (Not var)
 TDisj : forall f1 f2 tv, formulaTrue tv f1 \/ formulaTrue tv f2 > formula_map tv f1 > formula_map tv f2 >
formulaTrue tv (Disj f1 f2)
 TConj : forall f1 f2 tv, formulaTrue tv f1 > formulaTrue tv f2 > formula_map tv f1 > formula_map tv f2 >
formulaTrue tv (Conj f1 f2).
Definition checkOneMap (f : formula) (map : tvals) : {formulaTrue map f} + {~formulaTrue map f}. Admitted.
Definition fuel f := fact (length (vars_in_formula f)).
Eval compute in (fuel (Conj (Not 4) (Disj (Var 1) (Not 2)))).
Definition CheckFormulaHelp : forall f (fuel : nat) (ls : list nat) (map : tvals),
{truth : tvals  formulaTrue truth f } + {forall truth, ~formulaTrue truth f }.
refine (fix F f fuel ls map {struct fuel} : {truth : tvals  formulaTrue truth f } + {forall truth, ~formulaTrue truth f } :=
match fuel with
 0 => _
 S n => match ls return {truth : tvals  formulaTrue truth f } + {forall truth, ~formulaTrue truth f } with
 nil => match (checkOneMap f map) with
 left pf => _
 right pf => _
end
 x :: xs => match F f n xs (x !> Some true; map) with
 inright _ => F f n xs (x !> Some false; map)
 res => res
end
end
end).
 right.
 left. exists map. auto.
 admit.
Definition CheckFormula (f : formula) : {truth : tvals  formulaTrue truth f } + {forall truth, ~ formulaTrue truth f } := @CheckFormulaHelp f (fuel f) (vars_in_formula f) empty.
I need your advice… hint, direction, ideas…
Also some of my efforts here, all fruitless. sorry for the mess in code.
Thanks,
Natasha