ivy/test/ded1.ivy

#lang ivy1.7

include deduction

theorem [refl] {
    type t
    property X:t = X:t
}
proof
    apply introEq

theorem [symm] {
    type t
    property X:t = Y
    property Y:t = X
}
proof { 
    apply introEq;
    apply elimEq with x = X, y = Y
}

theorem [trans] {
    type t
    property X:t = Y
    property Y:t = Z
    property X:t = Z
}
proof {
    apply introEq;
    apply elimEq with x = Z, y = Y;
    apply symm;
    apply elimEq with x = Y, y = X;
    apply symm
}

theorem [cong1] {
    type t
    type u
    function f(X:t) : u
    property X:t = Y:t
    property f(X) = f(Y)
}
proof {
    apply introEq;
    apply elimEq with x = Y, y = X;
    apply symm
}

theorem [cong2] {
    type t1 
    type t2
    type u
    function f(X1:t1,X2:t2) : u
    property X1:t1 = Y1:t1
    property X2:t2 = Y2:t2
    property f(X1,X2) = f(Y1,Y2)
}
proof {
    apply introEq;
    apply elimEq with x = Y1, y = X1;
    apply symm;
    apply elimEq with x = Y2, y = X2;
    apply symm
}

theorem [cong3] {
    type t1 
    type t2
    type t3
    type u
    function f(X1:t1,X2:t2,X3:t3) : u
    property X1:t1 = Y1:t1
    property X2:t2 = Y2:t2
    property X3:t3 = Y3:t3
    property f(X1,X2,X3) = f(Y1,Y2,Y3)
}
proof {
    apply introEq;
    apply elimEq with x = Y1, y = X1;
    apply symm;
    apply elimEq with x = Y2, y = X2;
    apply symm;
    apply elimEq with x = Y3, y = X3;
    apply symm
}


theorem [commAnd] {
    relation p
    relation q
    property p & q
    property q & p
}
proof {
    apply introAnd;
    apply elimAndR;
    apply elimAndL
}

theorem [commOr] {
    relation p
    relation q
    property p | q
    property q | p
}
proof {
    apply elimOr with p = p, q = q;
    apply introOrR;
    apply introOrL
}

theorem [assocAnd] {
    relation p
    relation q
    relation r
    property (p & q) & r
    property p & (q & r)
}
proof {
    apply introAnd;
    apply elimAndL;
    apply elimAndL with q = r;
    apply introAnd;
    apply elimAndR;
    apply elimAndL with q = r;
    apply elimAndR with p = p & q, q = r
}


theorem [introNotNot] {
    relation p
    property p
    property ~~p
}
proof {
    apply exmid with p = ~~p, q = ~p;
    apply elimNot with q = ~~p, p = p
}

theorem [elimNotNot] {
    relation p
    property ~~p
    property p
}
proof {
    apply exmid with p = p, q = p;
    apply elimNot with q = p, p = ~p
}

theorem [reflImp] {
    relation p
    property p -> p
}
proof {
    apply introImp
}

theorem [thm1] {
    relation p
    relation q
    relation r
    property p & q
    property r
    property q & r
}
proof {
    apply introAnd;
    apply elimAndR with p = p
}

theorem [thm2] {
    relation p
    relation q
    relation r
    property p
    property ~~(q & r)
    property ~~p & r
}
proof {
    apply introAnd;
    apply introNot<s/q>;
    apply elimNot;
    apply elimAndR with q = r, p = q;
    apply elimNotNot
}

theorem [thm3] {
    relation p
    relation q
    relation r
    property p -> (q -> r)
    property p
    property ~r
    property ~q
}
proof {
    apply introNot<s/q>;
    apply elimNot with q = s, p = r;
    apply elimImp with q = r, p = q;
    apply elimImp with q = q -> r, p = p
}

theorem [thm4] {
    relation a
    relation b
    property ~b -> ~a
    property a -> ~~b
}
proof {
    apply introImp;
    apply introNot;
    apply elimNot with p = a;
    apply elimImp with p = ~b
}

theorem [thm5] {
    relation p
    relation q
    relation r
    property p & q -> r 
    property p -> (q -> r)
}
proof {
    apply introImp;
    apply introImp;
    apply elimImp with q = r, p = p & q;
    apply introAnd
}


theorem [thm6] {
    relation a
    relation b
    relation c
    property b -> c 
    property a | b -> a | c
}
proof {
    apply introImp;
    apply elimOr with p = a, q = b;
    apply introOrL;
    apply introOrR;
    apply elimImp with p = b
}

theorem [thm7] {
    relation a
    relation b
    relation c
    property a & (b | c)
    property (a & b) | (a & c)
}
proof {
    apply elimOr with p=b, q=c;
    apply introOrL;
    apply introAnd;
    apply elimAndL with q = b | c;
    apply introOrR;
    apply introAnd;
    apply elimAndL with q = b | c;
    apply elimAndR with p = a
}

theorem [thm8] {
    relation a
    relation b
    relation c
    property (a & b) | (a & c)
    property a & (b | c)
}
proof {
   apply elimOr with p = a & b, q = a & c;
   apply introAnd;
   apply elimAndL with q = b;
   apply introOrL;
   apply elimAndR with p = a;
   apply introAnd;
   apply elimAndL with q = c;
   apply introOrR;
   apply elimAndR with p = a
}


theorem [thm9] {
    relation a
    relation b
    property ~a | b
    property  a -> b
}
proof {
    apply introImp;
    apply elimOr with p = ~a, q = b;
    apply elimNot with p = a
}

theorem [thm10] {
    relation a
    relation b
    property a -> b
    property a -> ~b
    property ~a
}
proof {
    apply introNot;
    apply elimNot with p = b;
    apply elimImp with p = a;
    apply elimImp with p = a
}

theorem [modus_tollens] {
    relation p
    relation q
    property p -> q
    property ~q
    property ~p
}
proof {
    apply introNot<s/q>;
    apply elimNot with q = s, p = q;
    apply elimImp
}

theorem [exmid2] {
    relation p
    property p | ~p
}
proof {
    apply exmid with p = p | ~p, q = p;
    apply introOrL;
    apply introOrR
}

theorem [reductio] {
    relation p
    property ~p -> false
    property p
}
proof {
    apply elimNotNot;
    apply introNot;
    apply elimFalse;
    apply elimImp with p = ~p
}

theorem [pbc] {
    function p : bool
    property [absurd] { 
        property ~p
        property false
    }
    property p
}
proof {
    apply elimNotNot;
    apply introNot;
    apply elimFalse;
    apply absurd;
    showgoals
}


theorem [thm11] {
    type t
    individual x : t
    property x + 1 = 1 + x
    property (x + 1) > 1 -> (x + 1) > 0
    property (1 + x) > 1 -> (1 + x) > 0
}
proof { 
    apply elimEq with x = 1 + x, y = x + 1;
    apply symm
}

theorem [thm12] {
    type t
    function p(X:t) : bool
    function q(X:t) : bool
    property forall X. p(X) -> q(X)
    property forall X. p(X)
    property forall X. q(X)
}
proof {
    apply introA;
    apply elimImp with p=p(x), q=q(x);
    apply elimA with X = x;
    apply elimA with X = x
}


theorem [thm13] {
    type t
    individual z : t
    function p(X:t) : bool
    function q(X:t) : bool
    property p(z)
    property forall X. p(X) -> ~q(X)
    property ~q(z)
}
proof {
    apply elimImp with p = p(z);
    apply elimA with X = z
}

theorem [thm14] {
    type t
    function p(X:t) : bool
    property forall X. p(X)
    property exists X. p(X)
}
proof {
    apply introE;
    apply elimA with X = witness
}

theorem [thm15] {
    type t
    function p(X:t) : bool
    function q(X:t) : bool
    property forall X. p(X) -> q(X)
    property exists X. p(X)
    property exists X. q(X)
}
proof { 
    apply elimE with p(X) = p(X);
    apply introE with witness = x;
    apply elimImp with p = p(x);
    apply elimA with X = x
}

theorem [thm16] {
    type t
    function p(X:t) : bool
    function q(X:t) : bool
    property exists X. p(X)
    property forall X,Y. p(X) -> q(Y)
    property forall Y. q(Y)
}
proof {
    apply introA<y/x>;
    apply elimE with p(X) = p(X);
    apply elimImp with p = p(x);
    apply elimA with X = y;
    apply elimA<Z/Y> with X = x
}


# capture example
#
# theorem [thm17] {
#     type t
#     function p(X:t) : bool
#     function q(X:t) : bool
#     property exists X. p(X)
#     property forall X. (p(X) -> q(X))
#     property forall Y. q(Y)
# }
# proof {
#     apply introA;
#     apply elimE;
#     showgoals
# }

theorem [dualAE] {
    type t
    function p(X:t) : bool
    property ~forall X. p(X)
    property exists Y. ~p(Y)
}
proof {
    apply pbc;
    apply elimNot with p = forall X. p(X);
    apply introA;
    apply pbc;
    apply elimNot with p = exists Y. ~p(Y);
    apply introE with witness = x
}

theorem [dualEA] {
    type t
    function p(X:t) : bool
    property ~exists X. p(X)
    property forall Y. ~p(Y)
}
proof {
     apply introA;
     apply introNot;
     apply elimNot with p = exists X. p(X);
     apply introE with witness = x
}

theorem [dualAndOr] {
    relation p
    relation q
    property ~(p & q)
    property ~p | ~q
}
proof {
   apply pbc;
   apply elimNot with p = p & q;
   apply introAnd;
   apply pbc;
   apply elimNot with p =  ~p | ~q;
   apply introOrL;
   apply pbc;
   apply elimNot with p =  ~p | ~q;
   apply introOrR
}

theorem [dualOrAnd] {
    relation p
    relation q
    property ~(p | q)
    property ~p & ~q
}
proof {
     apply introAnd;
     apply introNot<r/q>;
     apply elimNot with p = p | q;
     apply introOrL;
     apply introNot<r/q>;
     apply elimNot with p = p | q;
     apply introOrR
}

theorem [andA1] {
    type t
    function p(X:t) : bool
    function q : bool
    property (forall X. p(X)) & q
    property forall X. p(X) & q
}
proof {
    apply introA;
    apply introAnd;
    apply elimA with X=x;
    apply elimAndL with q = q;
    apply elimAndR with p = forall X. p(X)
}

theorem [nonce] {
    type t
    individual x : t
    relation p
    property [triv] p
    property p
}
proof {
    apply triv
}

theorem [andA2] {
    type u
    function p(X:u) : bool
    function q : bool
    property forall X. p(X) & q
    property (forall X. p(X)) & q
}
proof {
    apply introAnd;
    apply introA;
    apply elimAndL with q = q;
    apply elimA with X=x;
    showgoals;
    apply nonce<u/t>;
    apply elimAndR with p = p(x);
    apply elimA with X=x
}


theorem [orE1] {
    type t
    function p(X:t) : bool
    function q(X:t) : bool
    property (exists X. p(X)) | (exists X. q(X))
    property exists X. p(X) | q(X)
}
proof {
    apply elimOr with p = exists X. p(X), q = exists X. q(X);
    apply elimE<r/q> with p(Z) = p(Z);
    apply introE with witness = x;
    apply introOrL;
    apply elimE<r/q> with p(Z) = q(Z);
    apply introE with witness = x;
    apply introOrR;
    showgoals
}

theorem [commE] {
    type t
    type u
    function p(X:t,Y:u) : bool
    property exists X. exists Y. p(X,Y)
    property exists Y. exists X. p(X,Y)
}
proof {
    apply elimE with p(X) = exists Y. p(X,Y);
    apply elimE<y/x> with p(X) = p(x,X);
    apply introE with witness = y;
    apply introE with witness = x;
    showgoals
}