-- File: bool2

-- defines not, and, and or as boolean functions

Path "../lol"
Load "bool"

---------
-- not --
---------

Def not := \b:Bool. if b false true

Prove not_true  : not true = false
Unfold not
Rewrite if_true
Refl
Exit

Prove not_false : not false = true
Unfold not
Rewrite if_false
Refl
Exit

Prove not_is_false_ : @b:Bool. not b = false -> b = true
Apply indbool
Intro
Refl
Intro
Lewrite H
Apply not_false
Exit

Prove not_is_true_ : @b:Bool. not b = true -> b = false
Apply indbool
Intro
Lewrite H
Apply not_true
Intro
Refl
Exit

Prove not_not : @b:Bool. not (not b) = b
Apply indbool
Rewrite not_true
Apply not_false 
Rewrite not_false
Apply not_true
Exit


---------
-- and --
---------

-- Name in lemmas: and
Def (&&) := \a,b:Bool. if a b false : Bool->Bool->Bool

Prove true_and : @b:Bool. true && b = b
Intro
Unfold (&&)
Rewrite if_true
Refl
Exit

Prove false_and : @b:Bool. false && b = false
Intro
Unfold (&&)
Rewrite if_false
Refl
Exit

Prove and_true : @b:Bool. b && true = b
Apply indbool 
Rewrite true_and
Refl
Rewrite false_and
Refl
Exit

Prove and_false : @b:Bool. b && false = false
Apply indbool 
Rewrite true_and
Refl
Rewrite false_and
Refl
Exit

Prove and_comm : @b,c:Bool. b && c = c && b
Intro
Apply indbool
Rewrite and_true
Rewrite true_and
Refl
Rewrite and_false
Rewrite false_and
Refl
Exit

Prove and_assoc : @b,c,d:Bool. (b&&c)&&d = b&&(c&&d)
Intro b,c
Apply indbool
Repeat Rewrite and_true
Refl
Repeat Rewrite and_false
Refl
Exit

Prove and_is_false_ : @b,c:Bool. b&&c = false -> b=false \/ c=false
Apply indbool Then Apply indbool
Rewrite true_and Then Intro Then OrIL Then Assumption
Intro Then OrIR Then Refl
Intro Then OrIL Then Refl
Intro Then OrIL Then Refl
Exit

Prove and_is_true_ : @b,c:Bool. b&&c = true -> b=true /\ c=true
Apply indbool Then Apply indbool
Intro Then AndI Then Refl
Rewrite true_and Then Intro Then AndI Then Try Refl Then Try Assumption
Rewrite false_and Then Intro Then AndI Then Try Refl Then Try Assumption
Rewrite false_and Then Intro Then AndI Then Assumption
Exit

--------
-- or --
--------

-- Name in lemmas: or
Def (||) := \a,b:Bool. if a true b : Bool->Bool->Bool

Prove true_or : @b:Bool. true || b = true
Intro
Unfold (||)
Rewrite if_true
Refl
Exit

Prove false_or : @b:Bool. false || b = b
Intro
Unfold (||)
Rewrite if_false
Refl
Exit

Prove or_true : @b:Bool. b || true = true
Apply indbool 
Rewrite true_or
Refl
Rewrite false_or
Refl
Exit

Prove or_false : @b:Bool. b || false = b
Apply indbool 
Rewrite true_or
Refl
Rewrite false_or
Refl
Exit

Prove or_comm : @b,c:Bool. b || c = c || b
Intro
Apply indbool
Rewrite or_true
Rewrite true_or
Refl
Rewrite or_false
Rewrite false_or
Refl
Exit

Prove or_assoc : @b,c,d:Bool. (b||c)||d = b||(c||d)
Intro b,c
Apply indbool
Repeat Rewrite or_true
Refl
Repeat Rewrite or_false
Refl
Exit

Prove or_idemp : @b:Bool. b||b = b
Apply indbool
Apply true_or
Apply false_or
Exit


Prove or_is_true_ : @b,c:Bool. b || c = true -> b=true \/ c=true
Apply indbool
Intros
OrIL
Refl
Apply indbool
Intro
OrIR
Refl
Rewrite false_or
Intro
OrIL
Assumption
Exit

Prove or_is_false_ : @b,c:Bool. b || c = false -> b=false /\ c=false
Apply indbool Then Apply indbool 
Rewrite true_or Then Intro Then AndI Then Try Assumption Then Try Refl
Rewrite true_or Then Intro Then AndI Then Try Assumption Then Try Refl
Rewrite false_or Then Intro Then AndI Then Try Assumption Then Try Refl
Rewrite false_or Then Intro Then AndI Then Try Assumption Then Try Refl
Exit

Prove not_or : @b,c:Bool. not (b||c) = not b && not c
Apply indbool Then Apply indbool
Rewrite true_or Then Repeat Rewrite not_true Then Rewrite false_and Then Refl
Rewrite true_or Then Repeat Rewrite not_true Then Rewrite not_false
Rewrite false_and Then Refl
Rewrite false_or Then Repeat Rewrite not_true Then Rewrite not_false
Rewrite true_and Then Refl
Rewrite false_or Then Repeat Rewrite not_false
Rewrite true_and Then Refl
Exit

Prove not_and : @b,c:Bool. not (b&&c) = not b || not c
Apply indbool Then Apply indbool
Rewrite true_and Then Repeat Rewrite not_true Then Rewrite false_or Then Refl
Rewrite true_and Then Rewrite not_true Then Repeat Rewrite not_false
Rewrite false_or Then Refl
Rewrite false_and Then Rewrite not_true Then Repeat Rewrite not_false
Rewrite true_or Then Refl
Rewrite false_and Then Repeat Rewrite not_false
Rewrite true_or Then Refl
Exit