Library Generate
Require Export SetChecker.
Require Export NArith.
Section Pythagoras.
Definition pythagorean (a b c:positive) := (a*a + b*b = c*c)%positive.
Lemma pythagorean_comm : forall a b c, pythagorean a b c -> pythagorean b a c.
Lemma pythagorean_neq_2 : forall a b c, pythagorean a b c -> b <> c.
Lemma pythagorean_neq_1 : forall a b c, pythagorean a b c -> a <> c.
Definition coloring := positive -> bool.
Definition pythagorean_pos (C:coloring) :=
forall a b c, pythagorean a b c -> (C a <> C b) \/ (C a <> C c) \/ (C b <> C c).
Definition pythagorean_neg (C:coloring) :=
forall a b c, C a = C b -> C a = C c -> ~pythagorean a b c.
Theorem pythagorean_equiv : forall C, pythagorean_pos C <-> pythagorean_neg C.
Definition pyth_lim_pos (n:positive) (C:coloring) :=
forall a b c, (a<n)%positive -> (b<n)%positive -> (c<n)%positive -> pythagorean a b c -> (C a <> C b) \/ (C a <> C c) \/ (C b <> C c).
Definition pyth_lim_neg (n:positive) (C:coloring) :=
forall a b c, (a<n)%positive -> (b<n)%positive -> (c<n)%positive -> C a = C b -> C a = C c -> ~pythagorean a b c.
Theorem pythagorean_lim_equiv : forall n C, pyth_lim_pos n C <-> pyth_lim_neg n C.
Lemma pyth_lim_gen : forall n C, pythagorean_pos C -> pyth_lim_pos n C.
Lemma pyth_lim_gen_neg : forall n C, ~pyth_lim_neg n C -> ~pythagorean_neg C.
Theorem no_pythagorean : forall n, (forall C, ~pyth_lim_pos n C) ->
forall C, ~pythagorean_pos C.
Lemma pythagorean_dec : forall a b c, {pythagorean a b c} + {~pythagorean a b c}.
End Pythagoras.
Section Lists_and_Stuff.
Definition target_list := list (list positive).
Definition ok_list (t:target_list) := forall tuple,
In tuple t -> exists a b c, tuple = (a::b::c::nil) /\ pythagorean a b c.
Definition colorful (C:coloring) (t:target_list) := forall tuple,
In tuple t -> exists a b, In a tuple /\ In b tuple /\ C a <> C b.
Fixpoint inner_cycle (n:positive) (m:nat) (b:positive) : target_list :=
match m with
| 0 => nil
| S m' => let mN := Pos.of_nat m in let sqrt := (Pos.sqrt (n*n+mN*mN)) in
if (sqrt<?b)%positive
then if pythagorean_dec n mN sqrt
then (mN::n::sqrt::nil) :: inner_cycle n m' b
else (inner_cycle n m' b)
else (inner_cycle n m' b)
end.
Lemma inner_cycle_okl : forall n m b, ok_list (inner_cycle n m b).
Fixpoint outer_cycle (n:nat) (b:positive) : target_list :=
match n with
| 0 => nil
| S m => (inner_cycle (Pos.of_nat n) n b) ++ (outer_cycle m b)
end.
Lemma outer_cycle_okl : forall n b, ok_list (outer_cycle n b).
Definition BPT_list (n:nat) := outer_cycle n (Pos.of_nat n).
End Lists_and_Stuff.
Section Lists_of_Clauses.
Definition posF (tuple:list positive) : Clause := map pos tuple.
Definition negF (tuple:list positive) : Clause := map neg tuple.
Fixpoint target_formula (t:target_list) : CNF :=
match t with
| nil => nil
| tuple::t' => (posF tuple) :: (negF tuple) :: (target_formula t')
end.
Lemma pos_in : forall a t, In a t -> In (pos a) (posF t).
Lemma neg_in : forall a t, In a t -> In (neg a) (negF t).
Lemma target_formula_in : forall a cl t, In (pos a) cl \/ In (neg a) cl ->
In cl (target_formula t) -> exists l, In a l /\ In l t.
Definition BPT_formula (n:nat) := target_formula (BPT_list n).
Lemma colorful_gives_val : forall C t,
colorful C t -> satisfies C (target_formula t).
Lemma val_gives_colorful : forall C t, satisfies C (target_formula t) ->
colorful C t.
Definition reduces (C C':CNF) := forall V, satisfies V C -> exists V', satisfies V' C'.
End Lists_of_Clauses.
Section Formula.
Parameter TheN : nat.
Definition The_CNF := BPT_formula TheN.
End Formula.
Lemma BPT_formula_sat : forall (C:coloring), pythagorean_pos C ->
forall n, satisfies C (BPT_formula n).
Theorem Pythagorean_Theorem : unsat The_CNF -> forall C, ~pythagorean_pos C.
Section Simplification.
Definition change_val (p:positive) (b:bool) (V:Valuation) :=
fun p' => if (p=?p')%positive then b else V p'.
Lemma change_val_p : forall p b V, change_val p b V p = b.
Lemma change_val_p' : forall p b V p', p <> p' -> change_val p b V p' = V p'.
Fixpoint no_occurrence (p:positive) (t:target_list) :=
match t with
| nil => True
| (l::t') => ~In p l /\ no_occurrence p t'
end.
Lemma no_occurrence_char : forall p t,
no_occurrence p t <-> forall l, In l t -> ~In p l.
Fixpoint one_occurrence (p:positive) (t:target_list) :=
match t with
| nil => False
| (l::t') => (In p l /\ no_occurrence p t')
\/ (~In p l /\ one_occurrence p t')
end.
Lemma one_occurrence_find : forall p t, one_occurrence p t ->
exists l, In p l /\ In l t /\ (forall l', In l' t -> l <> l' -> ~In p l').
Lemma colorful_add : forall t a, no_occurrence a t ->
forall C, colorful C t -> forall b, a <> b ->
forall l, In a l -> In b l -> exists C', colorful C' (l::t).
Lemma no_occurrence_add : forall t a, no_occurrence a t ->
forall b c, a <> b -> a <> c ->
reduces (target_formula t) (target_formula ((a::b::c::nil)::t)).
Fixpoint remove_number (p:positive) (t:target_list) :=
match t with
| nil => nil
| l::t' => if In_dec Pos.eq_dec p l then remove_number p t' else l::remove_number p t'
end.
Lemma remove_no_occurrence : forall p t, no_occurrence p (remove_number p t).
Lemma remove_keep : forall p t l, In l t -> ~In p l -> In l (remove_number p t).
Lemma remove_in : forall p t l, In l (remove_number p t) -> In l t.
Lemma colorful_remove_singleton : forall t a, one_occurrence a t -> ok_list t ->
forall C, colorful C (remove_number a t) ->
exists C', colorful C' t.
Lemma no_occurrence_dec : forall p t, {no_occurrence p t}+{~no_occurrence p t}.
Lemma one_occurrence_dec : forall p t, {one_occurrence p t}+{~one_occurrence p t}.
Fixpoint simplify (t:target_list) (l:list positive) :=
match l with
| nil => t
| p::l' => if (one_occurrence_dec p t) then simplify (remove_number p t) l'
else simplify t l'
end.
Lemma in_simplify : forall l l' t, In l' (simplify t l) -> In l' t.
Lemma colorful_simplify : forall t, ok_list t ->
forall l C, colorful C (simplify t l) -> exists C', colorful C' t.
Definition simplified_BPT_formula (n:nat) (l:list positive) :=
target_formula (simplify (BPT_list n) l).
Parameter The_List : list positive.
Definition The_Simple_CNF := simplified_BPT_formula TheN The_List.
Theorem simplification_ok : unsat The_CNF <-> unsat The_Simple_CNF.
Theorem Pythagorean_Theorem' : unsat The_Simple_CNF -> forall C, ~pythagorean_pos C.
End Simplification.
Section SymmetryBreak.
Lemma fix_one_color : forall C, pythagorean_pos C ->
forall n b, exists C', pythagorean_pos C' /\ C' n = b.
Parameter TheBreak : positive.
Definition The_Asymmetric_CNF : CNF :=
(pos TheBreak :: nil) :: simplified_BPT_formula TheN The_List.
Theorem symbreak_ok : unsat The_CNF <-> unsat The_Asymmetric_CNF.
Theorem Pythagorean_Theorem'' : unsat The_Asymmetric_CNF -> forall C, ~pythagorean_pos C.
End SymmetryBreak.
Require Export NArith.
Section Pythagoras.
Definition pythagorean (a b c:positive) := (a*a + b*b = c*c)%positive.
Lemma pythagorean_comm : forall a b c, pythagorean a b c -> pythagorean b a c.
Lemma pythagorean_neq_2 : forall a b c, pythagorean a b c -> b <> c.
Lemma pythagorean_neq_1 : forall a b c, pythagorean a b c -> a <> c.
Definition coloring := positive -> bool.
Definition pythagorean_pos (C:coloring) :=
forall a b c, pythagorean a b c -> (C a <> C b) \/ (C a <> C c) \/ (C b <> C c).
Definition pythagorean_neg (C:coloring) :=
forall a b c, C a = C b -> C a = C c -> ~pythagorean a b c.
Theorem pythagorean_equiv : forall C, pythagorean_pos C <-> pythagorean_neg C.
Definition pyth_lim_pos (n:positive) (C:coloring) :=
forall a b c, (a<n)%positive -> (b<n)%positive -> (c<n)%positive -> pythagorean a b c -> (C a <> C b) \/ (C a <> C c) \/ (C b <> C c).
Definition pyth_lim_neg (n:positive) (C:coloring) :=
forall a b c, (a<n)%positive -> (b<n)%positive -> (c<n)%positive -> C a = C b -> C a = C c -> ~pythagorean a b c.
Theorem pythagorean_lim_equiv : forall n C, pyth_lim_pos n C <-> pyth_lim_neg n C.
Lemma pyth_lim_gen : forall n C, pythagorean_pos C -> pyth_lim_pos n C.
Lemma pyth_lim_gen_neg : forall n C, ~pyth_lim_neg n C -> ~pythagorean_neg C.
Theorem no_pythagorean : forall n, (forall C, ~pyth_lim_pos n C) ->
forall C, ~pythagorean_pos C.
Lemma pythagorean_dec : forall a b c, {pythagorean a b c} + {~pythagorean a b c}.
End Pythagoras.
Section Lists_and_Stuff.
Definition target_list := list (list positive).
Definition ok_list (t:target_list) := forall tuple,
In tuple t -> exists a b c, tuple = (a::b::c::nil) /\ pythagorean a b c.
Definition colorful (C:coloring) (t:target_list) := forall tuple,
In tuple t -> exists a b, In a tuple /\ In b tuple /\ C a <> C b.
Fixpoint inner_cycle (n:positive) (m:nat) (b:positive) : target_list :=
match m with
| 0 => nil
| S m' => let mN := Pos.of_nat m in let sqrt := (Pos.sqrt (n*n+mN*mN)) in
if (sqrt<?b)%positive
then if pythagorean_dec n mN sqrt
then (mN::n::sqrt::nil) :: inner_cycle n m' b
else (inner_cycle n m' b)
else (inner_cycle n m' b)
end.
Lemma inner_cycle_okl : forall n m b, ok_list (inner_cycle n m b).
Fixpoint outer_cycle (n:nat) (b:positive) : target_list :=
match n with
| 0 => nil
| S m => (inner_cycle (Pos.of_nat n) n b) ++ (outer_cycle m b)
end.
Lemma outer_cycle_okl : forall n b, ok_list (outer_cycle n b).
Definition BPT_list (n:nat) := outer_cycle n (Pos.of_nat n).
End Lists_and_Stuff.
Section Lists_of_Clauses.
Definition posF (tuple:list positive) : Clause := map pos tuple.
Definition negF (tuple:list positive) : Clause := map neg tuple.
Fixpoint target_formula (t:target_list) : CNF :=
match t with
| nil => nil
| tuple::t' => (posF tuple) :: (negF tuple) :: (target_formula t')
end.
Lemma pos_in : forall a t, In a t -> In (pos a) (posF t).
Lemma neg_in : forall a t, In a t -> In (neg a) (negF t).
Lemma target_formula_in : forall a cl t, In (pos a) cl \/ In (neg a) cl ->
In cl (target_formula t) -> exists l, In a l /\ In l t.
Definition BPT_formula (n:nat) := target_formula (BPT_list n).
Lemma colorful_gives_val : forall C t,
colorful C t -> satisfies C (target_formula t).
Lemma val_gives_colorful : forall C t, satisfies C (target_formula t) ->
colorful C t.
Definition reduces (C C':CNF) := forall V, satisfies V C -> exists V', satisfies V' C'.
End Lists_of_Clauses.
Section Formula.
Parameter TheN : nat.
Definition The_CNF := BPT_formula TheN.
End Formula.
Lemma BPT_formula_sat : forall (C:coloring), pythagorean_pos C ->
forall n, satisfies C (BPT_formula n).
Theorem Pythagorean_Theorem : unsat The_CNF -> forall C, ~pythagorean_pos C.
Section Simplification.
Definition change_val (p:positive) (b:bool) (V:Valuation) :=
fun p' => if (p=?p')%positive then b else V p'.
Lemma change_val_p : forall p b V, change_val p b V p = b.
Lemma change_val_p' : forall p b V p', p <> p' -> change_val p b V p' = V p'.
Fixpoint no_occurrence (p:positive) (t:target_list) :=
match t with
| nil => True
| (l::t') => ~In p l /\ no_occurrence p t'
end.
Lemma no_occurrence_char : forall p t,
no_occurrence p t <-> forall l, In l t -> ~In p l.
Fixpoint one_occurrence (p:positive) (t:target_list) :=
match t with
| nil => False
| (l::t') => (In p l /\ no_occurrence p t')
\/ (~In p l /\ one_occurrence p t')
end.
Lemma one_occurrence_find : forall p t, one_occurrence p t ->
exists l, In p l /\ In l t /\ (forall l', In l' t -> l <> l' -> ~In p l').
Lemma colorful_add : forall t a, no_occurrence a t ->
forall C, colorful C t -> forall b, a <> b ->
forall l, In a l -> In b l -> exists C', colorful C' (l::t).
Lemma no_occurrence_add : forall t a, no_occurrence a t ->
forall b c, a <> b -> a <> c ->
reduces (target_formula t) (target_formula ((a::b::c::nil)::t)).
Fixpoint remove_number (p:positive) (t:target_list) :=
match t with
| nil => nil
| l::t' => if In_dec Pos.eq_dec p l then remove_number p t' else l::remove_number p t'
end.
Lemma remove_no_occurrence : forall p t, no_occurrence p (remove_number p t).
Lemma remove_keep : forall p t l, In l t -> ~In p l -> In l (remove_number p t).
Lemma remove_in : forall p t l, In l (remove_number p t) -> In l t.
Lemma colorful_remove_singleton : forall t a, one_occurrence a t -> ok_list t ->
forall C, colorful C (remove_number a t) ->
exists C', colorful C' t.
Lemma no_occurrence_dec : forall p t, {no_occurrence p t}+{~no_occurrence p t}.
Lemma one_occurrence_dec : forall p t, {one_occurrence p t}+{~one_occurrence p t}.
Fixpoint simplify (t:target_list) (l:list positive) :=
match l with
| nil => t
| p::l' => if (one_occurrence_dec p t) then simplify (remove_number p t) l'
else simplify t l'
end.
Lemma in_simplify : forall l l' t, In l' (simplify t l) -> In l' t.
Lemma colorful_simplify : forall t, ok_list t ->
forall l C, colorful C (simplify t l) -> exists C', colorful C' t.
Definition simplified_BPT_formula (n:nat) (l:list positive) :=
target_formula (simplify (BPT_list n) l).
Parameter The_List : list positive.
Definition The_Simple_CNF := simplified_BPT_formula TheN The_List.
Theorem simplification_ok : unsat The_CNF <-> unsat The_Simple_CNF.
Theorem Pythagorean_Theorem' : unsat The_Simple_CNF -> forall C, ~pythagorean_pos C.
End Simplification.
Section SymmetryBreak.
Lemma fix_one_color : forall C, pythagorean_pos C ->
forall n b, exists C', pythagorean_pos C' /\ C' n = b.
Parameter TheBreak : positive.
Definition The_Asymmetric_CNF : CNF :=
(pos TheBreak :: nil) :: simplified_BPT_formula TheN The_List.
Theorem symbreak_ok : unsat The_CNF <-> unsat The_Asymmetric_CNF.
Theorem Pythagorean_Theorem'' : unsat The_Asymmetric_CNF -> forall C, ~pythagorean_pos C.
End SymmetryBreak.