Logical Connectives

Conjunction

The conjunction (logical "and") in kind takes two propositions a and b, which should return a Boolean value true or false.

Bool.and (a: Bool) (b: Bool) : Bool
Bool.and Bool.true  b = b
Bool.and Bool.false b = Bool.false

If a is true, it is sufficient to return the value of b. However, if a is false, there is no need to verify the value of the second element.

Because it is a limited case (there are only two options), it is possible to verify with a simple proof:

ConjuntiveBool : Equal Bool (Bool.and Bool.true Bool.false) Bool.false
ConjuntiveBool = Equal.refl

And_exercise

And_exercise : Pair (Equal (Plus 3n 4n) 7n) (Equal (Mult 2n 2n) 4n)
And_exercise = ?

Both for proving conjunctive statements. To go in the other direction – that is, to use a conjunctive hypothesis to help prove something else – we employ pattern matching.

If the proof context contains a hypothesis h of the form (a,b), the case division will replace it with a pattern of pairs (a,b).

And_example2 (n: Nat) (m: Nat) (e: Pair (Equal n 0n) (Equal m 0n)) : Equal (Plus n m ) 0n
And_example2 Nat.zero Nat.zero e        = Equal.refl
And_example2 Nat.zero (Nat.succ m ) e   = 
    let p = (Equal.rewrite
    (Pair.snd e)
    (x => match Nat x {
        zero => Empty
        succ => Unit
    })
    (Unit.new))
    Empty.absurd p
And_example2 (Nat.succ n) m e           =
    let p = (Equal.rewrite
    (Pair.fst e)
    (x => match Nat x {
        zero => Empty
        succ => Unit 
    })
    (Unit.new))
    Empty.absurd p

You may wonder why we bother to group the two hypotheses n = 0 and m = 0 into a single conjunction, since we could also have declared the theorem with two separate premises:

And_example2a (n: Nat) (m: Nat) (e1: Equal n 0n) (e2: Equal m 0n) : Equal (Plus n m) 0n
And_example2a Nat.zero Nat.zero e1 e2        = Equal.refl
And_example2a Nat.zero (Nat.succ m ) e1 e2   = 
    let p = (Equal.rewrite
    (e2)
    (x => match Nat x {
        zero => Empty
        succ => Unit
    })
    (Unit.new))
    Empty.absurd p
And_example2a (Nat.succ n) m e1 e2           =
    let p = (Equal.rewrite
    (e1)
    (x => match Nat x {
        zero => Empty
        succ => Unit 
    })
    (Unit.new))
    Empty.absurd p

For this theorem, both formulations are adequate. But it is important to understand how to work with conjunctive hypotheses because conjunctions often arise from intermediate steps in proofs, especially in larger developments. Here is a simple example:

And_example3 (n: Nat) (m: Nat) (e: Equal (Plus n m) 0n) : Equal (Mult n m) 0n
And_example3 Nat.zero m e =  Equal.refl
And_example3 (Nat.succ n) m e =
    let p = (Equal.rewrite 
        (e)
        (x => match Nat x {
            zero => Empty 
            succ => Unit                      
        })
        (Unit.new))
    Empty.absurd p

Another common situation with conjunctions is that we know (a,b), but in some context we need only a (or only b). The following theorems are useful in such cases:

Proj1 <p> <q> (a: Pair p q) : p
Proj1 (Pair.new fst snd)    = fst

Proj2

Proj2 <p> <q> (b: Pair p q) : q
Proj2 (Pair.new fst snd)    = ?

Finally, sometimes we need to rearrange the order of the conjunctions and/or group the conjunctions of multiple paths. The following commutativity and associativity theorems are useful in such cases.

And_commut <p> <q> (c: Pair p q) : Pair q p
And_commut (Pair.new fst snd)    = Pair.new snd fst

And_assoc

And_assoc <p> <q> <r> (a: Pair p (Pair q r))  : Pair (Pair p q) r
And_assoc (Pair.new p (Pair q r) fst (Pair.new snd trd)) = ?

Disjunção

Another important connective is the disjunction, or logical "or", of two propositions:

Either a b is true when either a or b is true. The first case was marked with left, and the second with right.

To use a disjunctive hypothesis in a proof, we proceed by case analysis, which, as for Nat or other data types, can be done with pattern matching. Here is an example:

Or_example (n: Nat) (m: Nat) (e: (Either (Equal n 0n) (Equal m 0n))) : Equal (Mult n m) 0n
Or_example Nat.zero m e     = Equal.refl
Or_example n Nat.zero e     = Mult_0_r n
Or_example (Nat.succ n) m (Either.left l r val) = 
    let p = (Equal.rewrite
        (val)
        ( x => match Nat x {
            zero => Empty 
            succ => Unit            
        })
        (Unit.new))
    Empty.absurd p
Or_example (Nat.succ n) (Nat.succ m) (Either.right l r val) = 
    let p = (Equal.rewrite 
        (val)
        ( x => match Nat x {
            zero => Empty
            succ => Unit                   
        })
        (Unit.new))
Empty.absurd p

Conversely, to show that a disjunction is valid, we need to show that one of its sides is valid. This can be done through the Left and Right constructors mentioned above. Here is a trivial use...

axiom
Or_intro_left <a> <b> (t: a) : Either a b
Or_intro_left t = Either.left t

axiom
Or_intro_right <a> <b> (t: b) : Either a b
Or_intro_right t = Either.right t

... and a slightly more interesting example requiring both.

Zero_or_succ (n: Nat)     : Either (Equal n 0n) (Equal n (Nat.succ (Nat.pred n)))
Zero_or_succ Nat.zero     = Either.left  Equal.refl
Zero_or_succ (Nat.succ n) = Either.right Equal.refl

Mult_eq_0

axiom
Mult_eq_0 (n: Nat) (m: Nat) (e: Equal (Mult n m) 0n) : Either (Equal n 0n) (Equal m 0n)
Mult_eq_0 n m e = ?

Or_commut

Or_commut <p> <q> (e: Either p q) : Either q p
Or_commut e: ?