; (

(coq "Section Bg.")
(coq "Require Import Classical.")
(coq "Require Import Omega.")
(coq "Open Scope Z_scope.")

(trusted_rule
  (%initial SK F)
  (%known (%skol %NIL SK F)))

(trusted_rule
  (%final (%known false))
  %final_ok)

; If (%skol Q P A) rewrites to B then for any model M, M |= A there exists M', such that M' |= B,
; and vice versa.

; ------------- skol_rule starts ---------------
; id : forall a : Prop, a -> a.
(skol_rule 
  (%skol Q id A) 
  A)
(coq "intros. trivial. Qed.")

; pos_implies_def : forall a b : Prop, (a -> b) -> (~ a \/ b).
(skol_rule
  (%skol Q pos_implies_def (implies A B))  
  (or (not A) B))
(coq "intros. apply NNPP. tauto. Qed.")

; neg_implies_def : forall a b : Prop, ~(a -> b) -> ~(~ a \/ b).
(skol_rule
  (%skol Q neg_implies_def (not (implies A B)))
  (not (or (not A) B)))
(coq "intros. apply NNPP. tauto. Qed.")

; pos_iff_def : forall a b : Prop, (a <-> b) -> ((~ a \/ b) /\ (~ b \/ a)).
(skol_rule
  (%skol Q pos_iff_def (iff A B))  
  (and (or (not A) B) (or (not B) A)))
(coq "intros. apply NNPP. tauto. Qed.")

; neg_iff_def : forall a b : Prop, ~(a <-> b) -> ~((~ a \/ b) /\ (~ b \/ a)).
(skol_rule
  (%skol Q neg_iff_def (not (iff A B)))
  (not (and (or (not A) B) (or (not B) A))))
(coq "intros. apply NNPP. tauto. Qed.")

(skol_rule
  (%skol Q (and_or_distr X Y) (or (and A B) C))
  (and (%skol Q X (or A C)) (%skol Q Y (or B C))))
(coq "intros. elim H. elim H0. intros. exists x. exists x0. intro.
pose proof (H1 t) as H3. pose proof (H2 t) as H4. tauto. Qed.")

(skol_rule
  (%skol Q (or_and_distr X Y) (or A (and B C)))
  (and (%skol Q X (or A B)) (%skol Q Y (or A C))))
(coq "intros. elim H. elim H0. intros. exists x. exists x0. intro.
pose proof (H1 t) as H3. pose proof (H2 t) as H4. tauto. Qed.")

(skol_rule
  (%skol Q and_get (and A B))
  A)
(coq "intros. apply NNPP. tauto. Qed.")

(skol_rule
  (%skol Q and_skip (and A B))
  B)
(coq "intros. apply NNPP. tauto. Qed.")

; pos_and_comp : forall a a' b b' : Prop, (a -> a') -> (b -> b') -> (a /\ b -> a' /\ b').
(skol_rule
  (%skol Q (pos_and_comp X Y) (and A B))
  (and (%skol Q X A) (%skol Q Y B)))
(coq "intros. elim H. elim H0. intros. exists x. exists x0. intros.
pose proof (H1 t) as H4. pose proof (H2 t) as H5. tauto. Qed.")

; neg_and_comp : forall a a' b b' : Prop, (~a -> a') -> (~b -> b') -> (~(a /\ b) -> a' \/ b').
(skol_rule
  (%skol Q (neg_and_comp X Y) (not (and A B)))
  (or (%skol Q X (not A)) (%skol Q Y (not B))))
(coq "intros. elim H. elim H0. intros. exists x. exists x0. intros.
pose proof (H1 t) as H4. pose proof (H2 t) as H5. apply NNPP. tauto. Qed.")

; pos_or_comp : forall a a' b b' : Prop, (a -> a') -> (b -> b') -> (a \/ b -> a' \/ b').
(skol_rule
  (%skol Q (pos_or_comp X Y) (or A B))
  (or (%skol Q X A) (%skol Q Y B)))
(coq "intros. elim H. elim H0. intros. exists x. exists x0. intros.
pose proof (H1 t) as H4. pose proof (H2 t) as H5. tauto. Qed.")

; neg_or_comp : forall a a' b b' : Prop, (~a -> a') -> (~b -> b') -> (~(a \/ b) -> a' /\ b').
(skol_rule
  (%skol Q (neg_or_comp X Y) (not (or A B)))
  (and (%skol Q X (not A)) (%skol Q Y (not B))))
(coq "intros. elim H. elim H0. intros. exists x. exists x0. intros.
pose proof (H1 t) as H4. pose proof (H2 t) as H5. tauto. Qed.")

; or_comm : forall a b c d : Prop, ((b \/ c) -> d) -> (a \/ b) \/ c -> a \/ d.
(skol_rule
  (%skol Q (or_comm X) (or (or A B) C))
  (or A (%skol Q X (or B C))))
(coq "intros. elim H. intros. exists x. intros. pose proof (H0 t) as H2. tauto. Qed.")

(skol_rule
  (%skol Q (and_comm X) (and (and A B) C))
  (and A (%skol Q X (and B C))))
(coq "intros. elim H. intros. exists x. intros. pose proof (H0 t) as H2. tauto. Qed.")

; nnpp : forall a : Prop, (~ (~ a)) -> a.
(skol_rule
  (%skol Q nnpp (not (not A)))
  A)
(coq "intros. apply NNPP. tauto. Qed.")

(skol_rule
  (%skol Q (duplicate X Y) P)
  (and (%skol Q X P) (%skol Q Y P)))
(coq "intros. elim H. intros. exists x. intros. pose proof (H0 t) as H2. tauto. Qed.")

; TODO!
(trusted_rule
  (%skol Q eqtrue P)
  (= P true))
(trusted_rule
  (%skol Q eqtrue_neg (not P))
  (not (= P true)))

; ----------------- end skol_rule ---------------------

; compose : forall a b c : Prop, (b -> c) -> (a -> b) -> (a -> c).
(raw_coq_rule "
Lemma s_compose : forall T T0 T1 : Type,
        forall P0 : T -> T0 -> T1 -> Prop,
        forall P1 : T -> T1 -> Prop,
        forall A : T -> Prop,
        (exists f1 : T1, forall t : T, A t -> P1 t f1) ->
        (forall f1 : T1, exists f0 : T0, forall t : T, P1 t f1 -> P0 t f0 f1) ->
        exists f1 : T1, exists f0 : T0, forall t : T,
        A t -> P0 t f0 f1.
intros.  elim H.  intros.
pose proof (H0 x) as H2.
elim H2.  intros. 
exists x. exists x0.
 intros.
pose proof (H3 t) as H5.
pose proof (H1 t) as H6.
tauto.  Qed."
  (%skol Q (compose X Y) A)
  (%skol Q X (%skol Q Y A)))

(raw_coq_rule "
Require Import ClassicalChoice.
Lemma s_skolemize : forall T T2 : Type,
	T2 -> (* T2 is non empty *)
	forall P : T -> T2 -> Prop,
	exists f : T -> T2, forall t : T,
	((exists x : T2, P t x) -> P t (f t)).

intros. apply choice with (R := fun t ft => (exists x : T2, P t x) -> P t ft).
intros. assert ((exists x0 : T2, P x x0) -> exists y : T2, P x y).
intros.  elim H.  intros.  exists x0.  trivial.
assert (~(exists x0 : T2, P x x0) \/ (exists x0 : T2, P x x0)).
apply NNPP.  tauto.
intuition.  exists X.  tauto.  elim H1.  intros.  exists x0.  tauto.  Qed."
  (%skol Q (skolemize F) (exists P))
  (%BETA P (%SKOL F Q)))

(raw_coq_rule "
Lemma s_skip_forall : 
forall T1 T2 T3 : Type,
forall P1 : T2 -> T3 -> Prop,
forall P2 : T1 -> T2 -> T3 -> Prop,
  (exists f : T1, forall x : T2, forall y : T3, (P1 x y -> P2 f x y)) ->
  (exists f : T1, forall x : T2, (forall y : T3, P1 x y) -> (forall y : T3, P2 f x y)).
intros. elim H. intros.
exists x. intros.
pose proof (H0 x0 y) as H2.
pose proof (H1 y) as H3.
auto. Qed."
  (%skol Q (skip_forall R) (forall P))
  (forall (\ x (%skol (%CONS x Q) R (%BETA P x)))))

(raw_coq_rule "
Lemma s_norm_forall : forall T T2 : Type,
	forall P : T -> T2 -> Prop,
	forall t : T,
	(~(forall x : T2, P t x) -> exists x : T2, ~ P t x).
intros.  pose proof (not_all_ex_not T2 (P t) H). trivial. Qed."
  (%skol Q norm_forall (not (forall P)))
  (exists (\ x (not (%BETA P x)))))

(raw_coq_rule "
Lemma s_norm_exists : forall T T2 : Type,
        forall P : T -> T2 -> Prop,
        forall t : T,
        (~(exists x : T2, P t x) -> forall x : T2, ~ P t x).
intros.  pose proof (not_ex_all_not T2 (P t) H x) . trivial. Qed."
  (%skol Q norm_exists (not (exists P)))
  (forall (\ x (not (%BETA P x)))))

(raw_coq_rule "
Lemma remove_unused : forall T T2 : Type, forall P : T -> T2 -> Prop,
  T2 -> exists bogus : T2,
  (forall t : T, (forall x : T2, P t x) -> P t bogus).
intros. exists X. intros. apply H. Qed.
"
  (%skol Q (remove_unused R) (forall P))
  (%skol Q R (%BETA P bogus)))

; end %skol
;---------------------------------

; to_clause_1 : forall a b : Prop, ((a -> b) -> (a -> ~b -> False)).
(bool_rule
  (to_clause_1 (%known (implies A B)))
  (%known (implies A (implies (not B) false))))

; to_clause_2 : forall a b : Prop, ((a -> b) -> (~b -> a -> False)).
(bool_rule
  (to_clause_2 (%known (implies A B)))
  (%known (implies (not B) (implies A false))))

; to_clause_1_sn : forall a b : Prop, ((a -> ~b) -> (a -> b -> False)).
(bool_rule
  (to_clause_1_sn (%known (implies A (not B))))
  (%known (implies A (implies B false))))

; to_clause_2_sn : forall a b : Prop, ((a -> ~b) -> (b -> a -> False)).
(bool_rule
  (to_clause_2_sn (%known (implies A (not B))))
  (%known (implies B (implies A false))))

; absurd_n : forall a : Prop, (~a -> False) -> a.
(bool_rule
  (absurd_n (%known (implies (not X) false)))
  (%known X))

; absurd_p : forall a : Prop, (a -> False) -> ~a.
(bool_rule
  (absurd_p (%known (implies X false)))
  (%known (not X)))

; absurd_x : forall a : Prop, a -> (~a -> False).
(bool_rule
  (absurd_x (%known X))
  (%known (implies (not X) false)))

(bool_rule
  (absurd_x2 (%known (not X)))
  (%known (implies X false)))

; and_get : forall a b : Prop, a /\ b -> a.
(bool_rule
  (and_get (%known (and A B)))
  (%known A))

; and_skip : forall a b : Prop, a /\ b -> b.
(bool_rule
  (and_skip (%known (and A B)))
  (%known B))

; nor_get : forall a b : Prop, ~(a \/ b) -> ~a.
(bool_rule
  (nor_get (%known (not (or A B))))
  (%known (not A)))

; nor_skip : forall a b : Prop, ~(a \/ b) -> ~b.
(bool_rule
  (nor_skip (%known (not (or A B))))
  (%known (not B)))

; neg_unit_res : forall a b : Prop, a -> ~(a /\ b) -> ~b.
(bool_rule
  (neg_unit_res (%known A) (%known (not (and A B))))
  (%known (not B)))

; excl_mid_pn : forall a : Prop, a -> ~a -> False.
(bool_rule
  (excl_mid_pn (%known A) (%known (not A)))
  (%known false))

; excl_mid_np : forall a : Prop, ~a -> a -> False.
(bool_rule
  (excl_mid_np (%known (not A)) (%known A))
  (%known false))

(bool_rule
  (excl_mid_pn X (%known false))
  (%known false))

; unit_res_pn : forall a b : Prop, a -> (~ a \/ b) -> b.
(bool_rule
  (unit_res_pn (%known A) (%known (or (not A) B)))
  (%known B))

(bool_rule
  (unit_res_pn (%known true) (%known (or false B)))
  (%known B))

; unit_res_np : forall a b : Prop, ~a -> (a \/ b) -> b.
(bool_rule
  (unit_res_np (%known (not A)) (%known (or A B)))
  (%known B))

; it's kind of silly, but it generalizes
(bool_rule
  (simple_res_1_1 (%known (implies L false)))
  (%known (not L)))

(bool_rule
  (simple_res_2_1 (%known (implies L (implies A false))) (%known A))
  (%known (not L)))

(bool_rule
  (simple_res_2_2 (%known (implies A (implies L false))) (%known A))
  (%known (not L)))

(bool_rule
  (simple_res_3_1 (%known (implies L (implies A (implies B false)))) (%known A) (%known B))
  (%known (not L)))

(bool_rule
  (simple_res_3_2 (%known (implies A (implies L (implies B false)))) (%known A) (%known B))
  (%known (not L)))

(bool_rule
  (simple_res_3_3 (%known (implies A (implies B (implies L false)))) (%known A) (%known B))
  (%known (not L)))

(bool_rule
  (nnpp (%known (not (not L))))
  (%known L))

(bool_rule
  (id X)
  (%known (implies X X)))

(bool_rule
  (mp (%known (implies L X)) (%known L))
  (%known X))

; a hack
(trusted_rule
  true_false
  (%known (implies (not true) false)))


; --------- equality ---------

(eq_rule
  (eq_refl T)
  (%known (= T T)))

(eq_rule
  (eq_trans (%known (= A B)) (%known (= B C)))
  (%known (= A C)))

(eq_rule
  (eq_symm (%known (= A B)))
  (%known (= B A)))

(eq_rule
  (neq_symm (%known (not (= A B))))
  (%known (not (= B A))))

(raw_coq_rule "
Lemma k_eq_mon : forall T1 T2 : Type, forall P : T1 -> T2,
  forall a b : T1, a = b -> P a = P b.
congruence. Qed."
  (eq_mon P (%known (= A B)))
  (%known (= (%BETA P A) (%BETA P B))))

(raw_coq_rule "
Lemma k_eq_mon2 : forall T1 : Type, forall P : T1 -> Prop,
  forall a b : T1, a = b -> (P a -> P b).
congruence. Qed."
  (eq_mon2 P (%known (= A B)))
  (%known (implies (%BETA P A) (%BETA P B))))

(trusted_rule
  (eq_fake COMMENT T)
  (%known T))

(trusted_rule 
  (distinct_skip1 (%known (distinct A (distinct B C))))
  (%known (distinct B C)))

(trusted_rule 
  (distinct_skip2 (%known (distinct A (distinct B C))))
  (%known (distinct A C)))

(trusted_rule 
  (distinct_skip3 (%known (distinct A (distinct B C))))
  (%known (distinct A B)))

(trusted_rule 
  (distinct_to_neq (%known (distinct A B)))
  (%known (not (= A B))))


; -------------- arithmetic ------------------
; UTVPI canonical form: (<= (+ A B) C) or (<= A C)
; where A, B can be (~ t) and C is a constant

(arith_rule
  (arith_neg_lt (%known (not (< A B))))
  (%known (<= B A)))

(arith_rule
  (arith_neg_gt (%known (not (> A B))))
  (%known (<= A B)))

(arith_rule
  (arith_lt (%known (< A B)))
  (%known (<= (+ A 1) B)))

(arith_rule
  (arith_gt (%known (> A B)))
  (%known (<= (+ B 1) A)))

(arith_rule
  (arith_ge (%known (>= A B)))
  (%known (<= B A)))

(arith_rule
  (arith_neg_ge (%known (not (>= A B))))
  (%known (<= (+ A 1) B)))

(arith_rule
  (arith_neg_le (%known (not (<= A B))))
  (%known (<= (+ B 1) A)))

(arith_rule
  (arith_eq (%known (= A B)))
  (%known (<= A B)))

(arith_rule
  (arith_le_to_left (%known (<= A B)))
  (%known (<= (- A B) 0)))

(arith_rule
  (arith_move_1 (%known (<= A (+ B C))))
  (%known (<= (+ A (~ B)) C)))

(arith_rule
  (arith_move_2 (%known (<= (+ A B) C)))
  (%known (<= A (- C B))))

(arith_rule
  (utvpi_swap (%known (<= (+ A B) C)))
  (%known (<= (+ B A) C)))

(arith_rule
  (utvpi_trans (%known (<= (+ A B) C1))
               (%known (<= (+ (~ A) C) C2)))
  (%known (<= (+ B C) (%CONSTANT_FOLD (+ C1 C2)))))

(raw_coq_rule "
Lemma k_utvpi_tight : forall C2 C1 B A : Z, ((A + B) <= C1) -> ((-A + B) <= C2) -> (B + B <= ((C1 + C2) )).
intros. omega. Qed.  "
  (utvpi_tight (%known (<= (+ A B) C1))
               (%known (<= (+ (~ A) B) C2)))
  (%known (<= B (%CONSTANT_FOLD (%div (%CONSTANT_FOLD (+ C1 C2)) 2)))))

(arith_rule
  (utvpi_contr1 (%known (<= (+ A B) C1))
                (%known (<= (+ (~ A) (~ B)) C2)))
  (%known (%CONSTANT_FOLD (<= 0 (%CONSTANT_FOLD (+ C1 C2))))))

(arith_rule
  (utvpi_contr2 (%known (<= (+ A (~ B)) C1))
                (%known (<= (+ (~ A) B) C2)))
  (%known (%CONSTANT_FOLD (<= 0 (%CONSTANT_FOLD (+ C1 C2))))))

(raw_coq_rule "
Lemma k_utvpi_tight2 : forall C A : Z, ((A + A) <= C) -> ((A + 0) + (A + 0) <= (C )).
intros. omega. Qed.  "
  (utvpi_tight2 (%known (<= (+ A A) C)))
  (%known (<= (+ A 0) (%CONSTANT_FOLD (%div C 2)))))

(arith_rule
  (utvpi_contr_const (%known (<= (+ 0 0) C)))
  (%known (%CONSTANT_FOLD (<= 0 C))))

(arith_rule
  (plus_comm X Y W)
  (%known (= (+ (+ X Y) W) (+ X (+ Y W)))))

(arith_rule
  (plus_symm X Y)
  (%known (= (+ X Y) (+ Y X))))

(arith_rule
  (constant_fold X)
  (%known (= X (%CONSTANT_FOLD X))))


(arith_rule
  (arith_plus_norm (%known (= T1 (+ (+ A1 B1) C1)))
                   (%known (= T2 (+ (+ A2 B2) C2))))
  (%known (= (+ T1 T2) (+ (+ (%CONSTANT_FOLD (+ A1 A2)) (%CONSTANT_FOLD (+ B1 B2))) (%CONSTANT_FOLD (+ C1 C2))))))

(arith_rule
  (arith_plus_norm2 (%known (= T1 (+ (+ A1 0) C1)))
                    (%known (= T2 (+ (+ A2 0) C2))))
  (%known (= (+ T1 T2) (+ (+ A1 A2) (%CONSTANT_FOLD (+ C1 C2))))))

(arith_rule
  (arith_minus_norm (%known (= T1 (+ (+ A1 B1) C1)))
                    (%known (= T2 (+ (+ A2 B2) C2))))
  (%known (= (- T1 T2) (+ (+ (%CONSTANT_FOLD (- A1 A2)) (%CONSTANT_FOLD (- B1 B2))) (%CONSTANT_FOLD (- C1 C2))))))

(arith_rule
  (arith_minus_norm2 (%known (= T1 (+ (+ A1 0) C1)))
                     (%known (= T2 (+ (+ A2 0) C2))))
  (%known (= (- T1 T2) (+ (+ A1 (~ A2)) (%CONSTANT_FOLD (- C1 C2))))))

(arith_rule
  (arith_minus_norm3 (%known (= T1 (+ (+ A1 0) C1)))
                     (%known (= T2 (+ (+ (~ A2) 0) C2))))
  (%known (= (- T1 T2) (+ (+ A1 A2) (%CONSTANT_FOLD (- C1 C2))))))

(arith_rule
  (arith_neg_norm (%known (= T1 (+ (+ A1 B1) C1))))
  (%known (= (~ T1) (+ (+ (%CONSTANT_FOLD (- 0 A1)) (%CONSTANT_FOLD (- 0 B1))) (%CONSTANT_FOLD (- 0 C1))))))

(arith_rule
  (arith_neg_norm2 (%known (= T1 (+ (+ A1 B1) C1))))
  (%known (= (- T1) (+ (+ (%CONSTANT_FOLD (- 0 A1)) (%CONSTANT_FOLD (- 0 B1))) (%CONSTANT_FOLD (- 0 C1))))))

(arith_rule
  (arith_leq_norm (%known (= (- T1 T2) (+ (+ A1 B1) C1))) (%known (<= T1 T2)))
  (%known (<= (+ A1 B1) (%CONSTANT_FOLD (- 0 C1)))))

(arith_rule
  (minus_eq_def1 (%known (= (+ A (~ B)) C)))
  (%known (= A (+ B C))))

(arith_rule
  (minus_eq_def2 (%known (= (+ A (~ B)) C)))
  (%known (= B (+ A (%CONSTANT_FOLD (~ C))))))

(arith_rule
  (minus_eq_def1p (%known (= (+ A B) C)))
  (%known (= A (+ (~ B) C))))

(arith_rule
  (minus_eq_def2p (%known (= (+ A (~ B)) C)))
  (%known (= B (+ A (%CONSTANT_FOLD (~ C))))))

(arith_rule
  (utvpi_rev2 (%known (<= (+ (~ A) B) C)))
  (%known (<= (%CONSTANT_FOLD (~ C)) (+ A (~ B)))))

(arith_rule
  (utvpi_rev2p (%known (<= (+ (~ A) (~ B)) C)))
  (%known (<= (%CONSTANT_FOLD (~ C)) (+ A B))))

(arith_rule
  (utvpi_rev (%known (<= (+ (~ A) 0) C)))
  (%known (<= (%CONSTANT_FOLD (~ C)) A)))

(arith_rule
  (utvpi_drop_zero (%known (<= (+ A 0) C)))
  (%known (<= A C)))

(arith_rule
  (leq_antysymm (%known (<= C A)) (%known (<= A C)))
  (%known (= A C)))

(arith_rule
  (arith_var_norm V)
  (%known (= V (+ (+ V 0) 0))))

(arith_rule
  (arith_const_norm C)
  (%known (= C (+ (+ 0 0) C))))

(arith_rule
  (arith_mul2l T)
  (%known (= (* 2 T) (+ T T))))

(arith_rule
  (arith_mul2r T)
  (%known (= (* T 2) (+ T T))))


; --------------------
(raw_coq_rule "
Lemma inst : forall T T2 : Type, forall P1 : T -> T2 -> Prop,
  forall P2 : T -> Prop, T2 -> exists inst_t : T2,
    forall t : T, (P2 t -> forall x : T2, P1 t x) -> (P2 t -> P1 t inst_t).
intros. exists X. intros. apply H. trivial. Qed.
"
  (inst T (%known (implies X (forall P))))
  (%known (implies X (%BETA P T))))

(trusted_rule
  (assume L P)
  (%lift_known (implies L (%BETA P (%known L)))))

(trusted_rule
  (%lift_known (implies L (%known X)))
  (%known (implies L X)))

(trusted_rule
  (is_form (%known F) F)
  %ok)

(coq  "End Bg.")
; ---------- end prelude -------------
; )