Module unsat_proofs:lrat /* Variables are integers */ lit ::= pos(int) | neg(int) Projection lit : clause ::= emptyClause | or(lit, clause) Projection clause : formula ::= emptyFormula | and(clause, formula) Projection formula : /* Clause ID is an integer */ proof ::= emptyLrat(int, [int]) | addLrupProof(int, clause, [int], proof) | deleteLratProof(int, proof) Projection proof : [(int, clause)]
Module unsat_proofs:lrat Judgment sat_clause : [lit] clause* Judgment sat_formula : [lit] formula* mem L A ------------------------ [SC-Here] sat_clause A or(L, Rest) sat_clause A Rest ------------------------ [SC-Later] sat_clause A or(L, Rest) -------------------------- [SF-Empty] sat_formula A emptyFormula sat_clause A C sat_formula A Rest -------------------------- [SF-And] sat_formula A and(C, Rest) Judgment negate_lit : lit* lit ------------------------ [N-Pos] negate_lit pos(V) neg(V) ------------------------ [N-Neg] negate_lit neg(V) pos(V) Judgment unsat_clause : [lit] clause* -------------------------- [USC-EmptyClause] unsat_clause A emptyClause negate_lit L NL mem NL A unsat_clause A Rest -------------------------- [USC-Step] unsat_clause A or(L, Rest)
Module unsat_proofs:lrat Fixed Judgment proveFormula : formula proof formulaToKnown 1 F KnownClauses checkProof KnownClauses Prf =============================== [ProveFormula] proveFormula F Prf /*Turn a formula into a list of known clauses, numbering them with the first argument*/ Judgment formulaToKnown : int formula* [(int, clause)] --------------------------------- [FTK-Empty] formulaToKnown ID emptyFormula [] ID + 1 = NewID formulaToKnown NewID Rest KRest --------------------------------------------- [FTK-And] formulaToKnown ID and(C, Rest) (ID, C)::KRest Judgment checkProof : [(int, clause)] proof* rupProof Known emptyClause Prf ----------------------------------- [CP-EmptyLrat] checkProof Known emptyLrat(ID, Prf) remove_all Known ID KRest rupProof Known C Prf checkProof (ID, C)::KRest Rest ----------------------------------------------- [CP-AddLrup] checkProof Known addLrupProof(ID, C, Prf, Rest) select (ID, C) KRest Known checkProof KRest Rest ------------------------------------------ [CP-DeleteLrat] checkProof Known deleteLratProof(ID, Rest) Extensibella_Stand_In{ Known |{proof}- P ~~> P_P checkProof Known P_P ------------------------- [CP-Q] checkProof Known P } Judgment gatherLits : clause* [lit] ------------------------- [GL-EmptyClause] gatherLits emptyClause [] gatherLits Rest LRest ------------------------------- [GL-Or] gatherLits or(L, Rest) L::LRest Fixed Judgment negateLitList : [lit] [lit] =================== [NLL-Nil] negateLitList [] [] negate_lit L N negateLitList LRest NRest =================================== [NLL-Cons] negateLitList (L::LRest) (N::NRest) /*known clauses, clause, proof*/ Fixed Judgment rupProof : [(int, clause)] clause [int] /*known clauses, assignment, proof*/ Fixed Judgment rupProof_help : [(int, clause)] [lit] [int] gatherLits C Lits negateLitList Lits A rupProof_help Known A Prf ========================= [RUPP] rupProof Known C Prf lookup Known ID C unsat_clause A C ========================= [RUPPH-End] rupProof_help Known A [ID] lookup Known ID C unit_clause A C L rupProof_help Known L::A Prf ============================= [RUPPH-Step] rupProof_help Known A ID::Prf /*assignment, clause, unit ID*/ Judgment unit_clause : [lit] clause* lit !mem L A negate_lit L NL !mem NL A unsat_clause A C ------------------------ [UC-Here] unit_clause A or(L, C) L negate_lit L NL mem NL A unit_clause A C UL ------------------------- [UC-Later] unit_clause A or(L, C) UL /*remove all the bindings for the given ID succeeds even if no bindings are present*/ Fixed Judgment remove_all : [(int, clause)] int [(int, clause)] ================== [RA-Nil] remove_all [] I [] remove_all IRest I Rest =============================== [RA-Remove] remove_all (I, C)::IRest I Rest A != I remove_all IRest I Rest ======================================= [RA-Step] remove_all (A, C)::IRest I (A, C)::Rest
Click on a command or tactic to see a detailed view of its use.
Module unsat_proofs:lrat. /******************************************************************** * PROJECTIONS * ********************************************************************/ Projection_Constraint proj_lit_unique : forall L LA LB, ProjA : |{lit}- L ~~> LA -> ProjB : |{lit}- L ~~> LB -> LA = LB. Projection_Constraint proj_lit_is : forall L LT, Proj : |{lit}- L ~~> LT -> IsL : is_lit L -> is_lit LT. Projection_Constraint proj_clause_unique : forall C CA CB, ProjA : |{clause}- C ~~> CA -> ProjB : |{clause}- C ~~> CB -> CA = CB. Projection_Constraint proj_clause_is : forall C CT, Proj : |{clause}- C ~~> CT -> IsC : is_clause C -> is_clause CT. Projection_Constraint proj_formula_unique : forall F FA FB, ProjA : |{formula}- F ~~> FA -> ProjB : |{formula}- F ~~> FB -> FA = FB. Projection_Constraint proj_formula_is : forall F FT, Proj : |{formula}- F ~~> FT -> IsF : is_formula F -> is_formula FT. %Have proj_proof_is later because, relying on the known clauses as %the projection may, it might be it also relies on other relations %that use them, and then we want properties of them. /******************************************************************** * IS EXT_INDS * ********************************************************************/ Proj_Rel is_clause C. Ext_Ind forall C, is_clause C. [Show Proof] Proj_Rel is_formula F. Ext_Ind forall F, is_formula F. [Show Proof] /* Don't have Ext_Ind for is_proof because the projection can depend on the provability of the clause, so getting that for arbitrary proofs without adding checkProof is not possible, and adding checkProof is an unreasonable addition for Ext_Ind for is_proof. */ /******************************************************************** * DECIDABLE EQUALITY * ********************************************************************/ %Make this a fixed type as there is nothing else reasonable to add Extensible_Theorem is_lit_pos_or_neg : forall L, IsL : is_lit L -> exists I, L = pos I \/ L = neg I on IsL. [Show Proof] Theorem is_lit_eq_or_not : forall L1 L2, is_lit L1 -> is_lit L2 -> L1 = L2 \/ (L1 = L2 -> false). [Show Proof] Extensible_Theorem is_clause_empty_or_not : forall C, IsC : is_clause C -> emptyClause = C \/ (emptyClause = C -> false) on IsC. [Show Proof] Extensible_Theorem is_clause_or_or_not : forall C, IsC : is_clause C -> (exists L R, or L R = C) \/ ((exists L R, or L R = C) -> false) on IsC. [Show Proof] Extensible_Theorem is_clause_eq_or_not : forall C1 C2, IsC1 : is_clause C1 -> IsC2 : is_clause C2 -> C1 = C2 \/ (C1 = C2 -> false) on IsC1. [Show Proof] Extensible_Theorem is_formula_empty_or_not : forall F, IsF : is_formula F -> F = emptyFormula \/ (F = emptyFormula -> false) on IsF. [Show Proof] Extensible_Theorem is_formula_and_or_not : forall F, IsF : is_formula F -> (exists C F', F = unsat_proofs:lrat:and C F') \/ ((exists C F', F = unsat_proofs:lrat:and C F') -> false) on IsF. [Show Proof] Extensible_Theorem is_formula_eq_or_not : forall F1 F2, IsF1 : is_formula F1 -> IsF2 : is_formula F2 -> F1 = F2 \/ (F1 = F2 -> false) on IsF1. [Show Proof] Theorem is_list_integer_eq_or_not : forall L1 L2, is_list is_integer L1 -> is_list is_integer L2 -> L1 = L2 \/ (L1 = L2 -> false). [Show Proof] /******************************************************************** * LIST HELPERS * ********************************************************************/ Theorem lookup_after_select : forall Known ID ID' C C' KRest, is_list (is_pair is_integer is_clause) Known -> is_integer ID' -> (forall I C1 C2, mem (I, C1) Known -> mem (I, C2) Known -> C1 = C2) -> select (ID, C) KRest Known -> lookup KRest ID' C' -> lookup Known ID' C'. [Show Proof] Theorem mem_is : forall Known (IDC : pair integer clause), is_list (is_pair is_integer is_clause) Known -> mem IDC Known -> exists ID C, IDC = (ID, C) /\ is_integer ID /\ is_clause C. [Show Proof] Theorem mem_is_lit : forall Assignment L, is_list is_lit Assignment -> mem L Assignment -> is_lit L. [Show Proof] Theorem select_is : forall Known KRest IDC, is_list (is_pair is_integer is_clause) Known -> select IDC KRest Known -> is_list (is_pair is_integer is_clause) KRest. [Show Proof] Theorem select_is_picked : forall Known IDC KRest, is_list (is_pair is_integer is_clause) Known -> select IDC KRest Known -> is_pair is_integer is_clause IDC. [Show Proof] Theorem is_list_lit_mem_or_not : forall A L, is_list is_lit A -> is_lit L -> mem L A \/ (mem L A -> false). [Show Proof] Theorem is_list_lit_subset_or_not : forall A B, is_list is_lit A -> is_list is_lit B -> (forall X, mem X A -> mem X B) \/ exists X, mem X A /\ (mem X B -> false). [Show Proof] Theorem is_list_mem_lookup : forall Known ID C, is_list (is_pair is_integer is_clause) Known -> mem (ID, C) Known -> is_integer ID -> exists C', lookup Known ID C'. [Show Proof] Theorem lookup_is_value : forall K ID C, is_list (is_pair is_integer is_clause) K -> lookup K ID C -> is_clause C. [Show Proof] Theorem lookup_is_key : forall K ID C, is_list (is_pair is_integer is_clause) K -> lookup K ID C -> is_integer ID. [Show Proof] Theorem is_pair_eq_or_not : forall (PA PB : pair integer clause), is_pair is_integer is_clause PA -> is_pair is_integer is_clause PB -> PA = PB \/ (PA = PB -> false). [Show Proof] Theorem is_count_exists : forall L IDC, is_list (is_pair is_integer is_clause) L -> is_pair is_integer is_clause IDC -> exists N, count IDC L N. [Show Proof] Theorem all_count_0_nil : forall L, is_list (is_pair is_integer is_clause) L -> (forall X N, count X L N -> N = 0) -> L = []. [Show Proof] Theorem counts_permutation : forall L P, is_list (is_pair is_integer is_clause) L -> is_list (is_pair is_integer is_clause) P -> (forall X NL NP, is_pair is_integer is_clause X -> count X L NL -> count X P NP -> NL = NP) -> permutation L P. [Show Proof] Theorem selects_permutation : forall L P IDC LRest PRest, is_list (is_pair is_integer is_clause) L -> is_list (is_pair is_integer is_clause) P -> permutation L P -> select IDC LRest L -> select IDC PRest P -> permutation LRest PRest. [Show Proof] Theorem permutation_reflexive : forall L, is_list (is_pair is_integer is_clause) L -> permutation L L. [Show Proof] Theorem permutation_is : forall L P, is_list (is_pair is_integer is_clause) P -> permutation L P -> is_list (is_pair is_integer is_clause) L. [Show Proof] /******************************************************************** * SAT * ********************************************************************/ /*assignment only has L or -L, not both*/ Define good_assignment : list lit -> prop by good_assignment A := forall L NL, mem L A -> negate_lit L NL -> mem NL A -> false. Theorem good_assignment_sub : forall A B, good_assignment A -> (forall X, mem X B -> mem X A) -> good_assignment B. [Show Proof] Extensible_Theorem negate_lit_unique : forall L LA LB, IsL : is_lit L -> NegA : negate_lit L LA -> NegB : negate_lit L LB -> LA = LB on NegA. [Show Proof] Extensible_Theorem negate_lit_reverse : forall L NL, IsL : is_lit L -> Neg : negate_lit L NL -> negate_lit NL L on Neg. [Show Proof] Extensible_Theorem negate_lit_not_same : forall L, IsL : is_lit L -> Neg : negate_lit L L -> false on Neg. Extensible_Theorem negate_lit_is_lit : forall L NL, IsL : is_lit L -> Neg : negate_lit L NL -> is_lit NL on Neg. [Show Proof] Extensible_Theorem negate_lit_is_lit_back : forall L NL, IsNL : is_lit NL -> Neg : negate_lit L NL -> is_lit L on Neg. [Show Proof] Extensible_Theorem negate_lit_exists : forall L, IsL : is_lit L -> exists NL, negate_lit L NL on IsL. [Show Proof] %Projections are equisatisfiable with their projecting clauses Projection_Constraint sat_clause_ext_to_proj : forall C C' Sat, |{clause}- C ~~> C' -> is_list is_lit Sat -> is_clause C -> sat_clause Sat C -> sat_clause Sat C'. Projection_Constraint sat_clause_proj_to_ext : forall C C' Sat, |{clause}- C ~~> C' -> is_list is_lit Sat -> is_clause C -> sat_clause Sat C' -> sat_clause Sat C. Projection_Constraint unsat_clause_ext_to_proj : forall C C' Unsat, |{clause}- C ~~> C' -> is_list is_lit Unsat -> is_clause C -> unsat_clause Unsat C -> unsat_clause Unsat C'. Projection_Constraint unsat_clause_proj_to_ext : forall C C' Unsat, |{clause}- C ~~> C' -> is_list is_lit Unsat -> is_clause C -> unsat_clause Unsat C' -> unsat_clause Unsat C. %Projections are equisatisfiable with their projecting formulas Projection_Constraint sat_formula_ext_to_proj : forall F F' Sat, |{formula}- F ~~> F' -> is_list is_lit Sat -> sat_formula Sat F -> sat_formula Sat F'. Projection_Constraint sat_formula_proj_to_ext : forall F F' Sat, |{formula}- F ~~> F' -> is_list is_lit Sat -> sat_formula Sat F' -> sat_formula Sat F. Extensible_Theorem unsat_sat_clause : forall A C, IsC : is_clause C -> IsA : is_list is_lit A -> UNSAT : unsat_clause A C -> SAT : sat_clause A C -> GA : good_assignment A -> false on UNSAT. [Show Proof] Extensible_Theorem sat_clause_orderless : forall A1 A2 C, IsC : is_clause C -> IsA1 : is_list is_lit A1 -> IsA2 : is_list is_lit A2 -> SAT : sat_clause A1 C -> MemA1A2 : (forall L, mem L A1 -> mem L A2) -> sat_clause A2 C on SAT. [Show Proof] Extensible_Theorem sat_formula_orderless : forall A1 A2 F, IsF : is_formula F -> IsA1 : is_list is_lit A1 -> IsA2 : is_list is_lit A2 -> SAT : sat_formula A1 F -> MemA1A2 : (forall L, mem L A1 -> mem L A2) -> sat_formula A2 F on SAT. [Show Proof] Extensible_Theorem unsat_clause_orderless : forall A1 A2 C, IsC : is_clause C -> IsA1 : is_list is_lit A1 -> IsA2 : is_list is_lit A2 -> UNSAT : unsat_clause A1 C -> MemA1A2 : (forall L, mem L A1 -> mem L A2) -> unsat_clause A2 C on UNSAT. [Show Proof] /******************************************************************** * UNSAT PROOFS * ********************************************************************/ Extensible_Theorem unit_clause_is : forall A C L, IsC : is_clause C -> IsA : is_list is_lit A -> Unit : unit_clause A C L -> is_lit L on Unit. [Show Proof] Extensible_Theorem unit_clause_unique : forall A B C LA LB, IsC : is_clause C -> IsA : is_list is_lit A -> IsB : is_list is_lit B -> UnitA : unit_clause A C LA -> UnitB : unit_clause B C LB -> Prm : permutation A B -> LA = LB on UnitA. [Show Proof] Extensible_Theorem unit_clause_not_assigned : forall A C L, IsC : is_clause C -> IsA : is_list is_lit A -> UC : unit_clause A C L -> Mem : mem L A -> false on UC. [Show Proof] Extensible_Theorem unit_clause_not_assigned_negate : forall A C L NL, IsC : is_clause C -> IsA : is_list is_lit A -> UC : unit_clause A C L -> Neg : negate_lit L NL -> Mem : mem NL A -> false on UC. [Show Proof] Extensible_Theorem unit_clause_expand : forall A C L E, IsC : is_clause C -> IsA : is_list is_lit A -> IsE : is_list is_lit E -> UC : unit_clause A C L -> SAT : sat_clause E C -> GA_A : good_assignment A -> GA_E : good_assignment E -> Expand : (forall L, mem L A -> mem L E) -> mem L E on UC. [Show Proof] Extensible_Theorem unit_clause_add : forall A S C L, IsC : is_clause C -> IsA : is_list is_lit A -> IsS : is_list is_lit S -> UC : unit_clause A C L -> Mem : mem L S -> sat_clause S C on UC. [Show Proof] Theorem remove_all_no_lookup : forall Known ID KRest, remove_all Known ID KRest -> no_lookup KRest ID. [Show Proof] Theorem remove_all_no_mem : forall Known ID KRest C, remove_all Known ID KRest -> mem (ID, C) KRest -> false. [Show Proof] Theorem remove_all_still_mem : forall Known ID KRest Other C, remove_all Known ID KRest -> mem (Other, C) Known -> (ID = Other -> false) -> mem (Other, C) KRest. [Show Proof] Theorem remove_all_mem_after : forall Known ID KRest Other C, remove_all Known ID KRest -> mem (Other, C) KRest -> mem (Other, C) Known. [Show Proof] Theorem remove_all_lookup_after : forall Known KRest ID Other C, remove_all Known ID KRest -> lookup KRest Other C -> lookup Known Other C. [Show Proof] Theorem remove_all_is : forall Known ID KRest, is_list (is_pair is_integer is_clause) Known -> remove_all Known ID KRest -> is_list (is_pair is_integer is_clause) KRest. [Show Proof] Theorem is_remove_all_exists : forall Known ID, is_list (is_pair is_integer is_clause) Known -> is_integer ID -> exists KRest, remove_all Known ID KRest. [Show Proof] Theorem remove_all_counts : forall Known ID KRest IDC N, remove_all Known ID KRest -> count IDC Known N -> ((exists C, IDC = (ID, C)) -> false) -> count IDC KRest N. [Show Proof] Theorem remove_all_permutation : forall Known ID KRest P, is_list (is_pair is_integer is_clause) Known -> is_integer ID -> remove_all Known ID KRest -> permutation Known P -> exists P', remove_all P ID P' /\ permutation KRest P'. [Show Proof] %a good clause list contains at most one binding for each ID Define good_clause_list : list (pair integer clause) -> prop by good_clause_list Known := forall ID C1 KRest C2, select (ID, C1) KRest Known -> mem (ID, C2) KRest -> false. Theorem good_clause_list_drop : forall L IDC, good_clause_list ((IDC)::L) -> good_clause_list L. [Show Proof] Theorem good_clause_list_select : forall L Rest ID C, good_clause_list L -> select (ID, C) Rest L -> good_clause_list Rest. [Show Proof] Theorem good_clause_list_remove_all : forall Known ID KRest, good_clause_list Known -> remove_all Known ID KRest -> good_clause_list KRest. [Show Proof] Theorem good_clause_list_add : forall Known ID C, good_clause_list Known -> ((exists C', mem (ID, C') Known) -> false) -> good_clause_list ((ID, C)::Known). [Show Proof] Theorem good_clause_list_remove_all_add : forall Known ID KRest C, good_clause_list Known -> remove_all Known ID KRest -> good_clause_list ((ID, C)::KRest). [Show Proof] Theorem permutation_good_clause_list : forall L P, is_list (is_pair is_integer is_clause) P -> permutation L P -> good_clause_list L -> good_clause_list P. [Show Proof] Theorem good_clause_list_mems : forall L X CA CB, good_clause_list L -> mem (X, CA) L -> mem (X, CB) L -> CA = CB. [Show Proof] Theorem rupProof_help_all_mem : forall Known A Proof ID, rupProof_help Known A Proof -> mem ID Proof -> exists C, lookup Known ID C. [Show Proof] Theorem rupProof_help_is : forall Known A Proof, rupProof_help Known A Proof -> is_list (is_pair is_integer is_clause) Known -> is_list is_integer Proof. [Show Proof] Theorem rupProof_help_unsat : forall Known A Sat Proof, is_list (is_pair is_integer is_clause) Known -> is_list is_lit A -> is_list is_lit Sat -> %Having both rup_help (a successful proof line) rupProof_help Known A Proof -> %and a superset satisfying assignment (forall (L : lit), mem L A -> mem L Sat) -> (forall (InID : integer) (InC : clause), lookup Known InID InC -> sat_clause Sat InC) -> %that is a good assignment good_assignment A -> good_assignment Sat -> %is impossible false. [Show Proof] Theorem rupProof_help_orderless : forall K1 K2 A Prf, is_list (is_pair is_integer is_clause) K1 -> is_list (is_pair is_integer is_clause) K2 -> good_clause_list K2 -> rupProof_help K1 A Prf -> (forall ID C, mem (ID, C) K1 -> mem (ID, C) K2) -> rupProof_help K2 A Prf. [Show Proof] Extensible_Theorem gatherLits_is : forall C L, IsC : is_clause C -> GL : gatherLits C L -> is_list is_lit L on GL. [Show Proof] Extensible_Theorem gatherLits_exists : forall C, IsC : is_clause C -> exists L, gatherLits C L on IsC. [Show Proof] Extensible_Theorem gatherLits_permutation : forall C L1 L2, IsC : is_clause C -> GL1 : gatherLits C L1 -> GL2 : gatherLits C L2 -> permutation L1 L2 on GL1. [Show Proof] Projection_Constraint proj_gatherLits : forall C C' L, |{clause}- C ~~> C' -> is_clause C -> gatherLits C L -> exists L', gatherLits C' L'. Projection_Constraint proj_gatherLits_permutation : forall C C' L L', |{clause}- C ~~> C' -> is_clause C -> gatherLits C L -> gatherLits C' L' -> permutation L L'. Extensible_Theorem gatherLits_sat : forall C Lits Sat, IsC : is_clause C -> IsSat : is_list is_lit Sat -> GL : gatherLits C Lits -> Sat : sat_clause Sat C -> exists L, mem L Lits /\ mem L Sat on Sat. [Show Proof] Extensible_Theorem gatherLits_mem_sat : forall C Lits Sat L, IsC : is_clause C -> IsSat : is_list is_lit Sat -> GL : gatherLits C Lits -> MemLits : mem L Lits -> MemSat : mem L Sat -> sat_clause Sat C on GL. [Show Proof] Extensible_Theorem gatherLits_unsat : forall C Lits Unsat L, GA : good_assignment Unsat -> IsC : is_clause C -> IsUnsat : is_list is_lit Unsat -> GL : gatherLits C Lits -> Unsat : unsat_clause Unsat C -> MemLits : mem L Lits -> MemUnsat : mem L Unsat -> false on Unsat. [Show Proof] Theorem negateLitList_is : forall L NL, is_list is_lit L -> negateLitList L NL -> is_list is_lit NL. [Show Proof] Theorem negateLitList_exists : forall L, is_list is_lit L -> exists NL, negateLitList L NL. [Show Proof] Theorem negateLitList_mem_negate_before : forall X NL L NX, is_list is_lit NL -> mem X NL -> negateLitList L NL -> negate_lit X NX -> mem NX L. [Show Proof] Extensible_Theorem negate_lits_unsat : forall C L NL, IsC : is_clause C -> GL : gatherLits C L -> NLL : negateLitList L NL -> unsat_clause NL C on GL. [Show Proof] Theorem rupProof_all_mem : forall Known C Proof ID, rupProof Known C Proof -> mem ID Proof -> exists C', lookup Known ID C'. [Show Proof] Theorem rupProof_is : forall Known C Proof, rupProof Known C Proof -> is_list (is_pair is_integer is_clause) Known -> is_list is_integer Proof. [Show Proof] Theorem rupProof_maintains_sat : forall Known C Prf Sat, is_list (is_pair is_integer is_clause) Known -> is_list is_lit Sat -> rupProof Known C Prf -> (forall ID InC, lookup Known ID InC -> sat_clause Sat InC) -> is_clause C -> is_list is_lit Sat -> good_assignment Sat -> exists S, is_list is_lit S /\ good_assignment S /\ (forall L, mem L Sat -> mem L S) /\ sat_clause S C. [Show Proof] Theorem rupProof_orderless : forall K1 K2 C Prf, is_list (is_pair is_integer is_clause) K1 -> is_list (is_pair is_integer is_clause) K2 -> good_clause_list K2 -> rupProof K1 C Prf -> (forall ID C', mem (ID, C') K1 -> mem (ID, C') K2) -> rupProof K2 C Prf. [Show Proof] Theorem rupProof_permutation : forall K1 K2 C Prf, is_list (is_pair is_integer is_clause) K1 -> is_list (is_pair is_integer is_clause) K2 -> good_clause_list K2 -> rupProof K1 C Prf -> permutation K1 K2 -> rupProof K2 C Prf. [Show Proof] /******************************************************************** * CHECK PROOF * ********************************************************************/ /* Don't have proj_proof_unique because there could be multiple ways to prove a clause, so it doesn't necessarily make sense to say the proof hint needs to be the same */ Projection_Constraint proj_proof_is : forall Known P PT, Proj : Known |{proof}- P ~~> PT -> IsP : is_proof P -> IsKnown : is_list (is_pair is_integer is_clause) Known -> GCL : good_clause_list Known -> is_proof PT. /* While it isn't unique, we can get the same projection with an extended clause set, since all the clauses we need for the proof are present in both. */ Projection_Constraint proj_proof_extend : forall Known P PT Known', Proj : Known |{proof}- P ~~> PT -> IsP : is_proof P -> IsKnown : is_list (is_pair is_integer is_clause) Known -> IsKnown' : is_list (is_pair is_integer is_clause) Known' -> GCL : good_clause_list Known -> GCL' : good_clause_list Known' -> Mems : (forall ID C, mem (ID, C) Known -> mem (ID, C) Known') -> Known' |{proof}- P ~~> PT. %lemma for the next theorem Theorem sat_lemma : forall ID C Known KRest S, (forall CID InC, lookup ((ID, C)::Known) CID InC -> sat_clause S InC) -> remove_all Known ID KRest -> forall CID InC, lookup ((ID, C)::KRest) CID InC -> sat_clause S InC. [Show Proof] Extensible_Theorem check_proof_correct : forall Known P Sat, IsP : is_proof P -> IsSat : is_list is_lit Sat -> GA_Sat : good_assignment Sat -> GCL : good_clause_list Known -> IsKnown : is_list (is_pair is_integer is_clause) Known -> %The unsat proof checks out CP : checkProof Known P -> %and there is a satisfying assignment for the existing clauses--- Sat : (forall CID C, lookup Known CID C -> sat_clause Sat C) -> %this is impossible false on CP. [Show Proof] Extensible_Theorem checkProof_orderless : forall K1 K2 Prf, IsP : is_proof Prf -> IsK1 : is_list (is_pair is_integer is_clause) K1 -> IsK2 : is_list (is_pair is_integer is_clause) K2 -> GCL : good_clause_list K2 -> CP : checkProof K1 Prf -> Prm : permutation K1 K2 -> checkProof K2 Prf on CP. [Show Proof] Ext_Size checkProof Known P. Proj_Rel checkProof Known P. Ext_Ind forall Known P, checkProof Known P with IsP : is_proof P, IsKnown : is_list (is_pair is_integer is_clause) Known, GCL : good_clause_list Known. [Show Proof] %Projected proof still checks out Projection_Constraint proj_checkProof : forall Known P P', Known |{proof}- P ~~> P' -> checkProof Known P -> is_list (is_pair is_integer is_clause) Known -> good_clause_list Known -> checkProof Known P'. /******************************************************************** * PROVE FORMULA * ********************************************************************/ Extensible_Theorem formulaToKnown_unique : forall F ID KA KB, IsF : is_formula F -> IsID : is_integer ID -> FTKA : formulaToKnown ID F KA -> FTKB : formulaToKnown ID F KB -> KA = KB on FTKA. [Show Proof] Extensible_Theorem formulaToKnown_all_greater : forall F ID K CID C, FTK : formulaToKnown ID F K -> Mem : mem (CID, C) K -> IsID : is_integer ID -> CID >= ID on FTK. [Show Proof] Extensible_Theorem formulaToKnown_all_unique : forall F ID K CID CA KRest CB, FTK : formulaToKnown ID F K -> IsID : is_integer ID -> Slct : select (CID, CA) KRest K -> Mem : mem (CID, CB) KRest -> false on FTK. [Show Proof] Extensible_Theorem formulaToKnown_sat_formula : forall F ID K A CID C, FTK : formulaToKnown ID F K -> Sat : sat_formula A F -> Mem : mem (CID, C) K -> sat_clause A C on FTK. [Show Proof] Extensible_Theorem formulaToKnown_is : forall F ID K, IsF : is_formula F -> IsID : is_integer ID -> FTK : formulaToKnown ID F K -> is_list (is_pair is_integer is_clause) K on FTK. [Show Proof] Theorem proveFormula_correct : forall F Prf Sat, is_formula F -> is_proof Prf -> is_list is_lit Sat -> good_assignment Sat -> %proof checking out and formula satisfiable proveFormula F Prf -> sat_formula Sat F -> %is impossible false. [Show Proof]