Load tactics.

(*
3.20 (page 86)
*)
Example E3_20 Object (P Q:Object*Object->Prop):
    (forall x y, P(x,y) -> Q(y,x)) /\ (forall x, P(x,x)) -> forall y, Q(y,y).
Object: Type
P, Q: Object * Object -> Prop
(forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x)) ->
forall y : Object, Q (y, y)
Proof.
Object: Type
P, Q: Object * Object -> Prop
(forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x)) ->
forall y : Object, Q (y, y)
    impl_intro.
Object: Type
P, Q: Object * Object -> Prop
H0: (forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x))
forall y : Object, Q (y, y)
    and_elim H0.
Object: Type
P, Q: Object * Object -> Prop
H0: (forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x))
H1: forall x y : Object, P (x, y) -> Q (y, x)
H2: forall x : Object, P (x, x)
forall y : Object, Q (y, y)
    forall_intro z.
Object: Type
P, Q: Object * Object -> Prop
H0: (forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x))
H1: forall x y : Object, P (x, y) -> Q (y, x)
H2: forall x : Object, P (x, x)
z: Object
Q (z, z)
    forall_elim H1 z.
Object: Type
P, Q: Object * Object -> Prop
H0: (forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x))
H1: forall x y : Object, P (x, y) -> Q (y, x)
H2: forall x : Object, P (x, x)
z: Object
H3: forall y : Object, P (z, y) -> Q (y, z)
Q (z, z)
    forall_elim H3 z.
Object: Type
P, Q: Object * Object -> Prop
H0: (forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x))
H1: forall x y : Object, P (x, y) -> Q (y, x)
H2: forall x : Object, P (x, x)
z: Object
H3: forall y : Object, P (z, y) -> Q (y, z)
H4: P (z, z) -> Q (z, z)
Q (z, z)
    impl_apply H4.
Object: Type
P, Q: Object * Object -> Prop
H0: (forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x))
H1: forall x y : Object, P (x, y) -> Q (y, x)
H2: forall x : Object, P (x, x)
z: Object
H3: forall y : Object, P (z, y) -> Q (y, z)
H4: P (z, z) -> Q (z, z)
P (z, z)
    forall_elim H2 z.
Object: Type
P, Q: Object * Object -> Prop
H0: (forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x))
H1: forall x y : Object, P (x, y) -> Q (y, x)
H2: forall x : Object, P (x, x)
z: Object
H3: forall y : Object, P (z, y) -> Q (y, z)
H4: P (z, z) -> Q (z, z)
H5: P (z, z)
P (z, z)
    assumption H5.
Restart. (* lets try it with Coq tactics *)
Object: Type
P, Q: Object * Object -> Prop
(forall x y : Object, P (x, y) -> Q (y, x)) /\
(forall x : Object, P (x, x)) ->
forall y : Object, Q (y, y)
    intros [H1 H2] y.
Object: Type
P, Q: Object * Object -> Prop
H1: forall x y : Object, P (x, y) -> Q (y, x)
H2: forall x : Object, P (x, x)
y: Object
Q (y, y)
    apply H1.
Object: Type
P, Q: Object * Object -> Prop
H1: forall x y : Object, P (x, y) -> Q (y, x)
H2: forall x : Object, P (x, x)
y: Object
P (y, y)
    apply H2.
Qed.


(*
3.30 (page 92)
*)
Example E3_30: forall (x:nat), x <= x.
forall x : nat, x <= x
Proof.
forall x : nat, x <= x
    forall_intro x.
x: nat
x <= x
    exists_intro 0.
x: nat
x + 0 = x
    axiom add_0_r.
x: nat
A0: forall n : nat, n + 0 = n
x + 0 = x
    forall_elim A0 x.
x: nat
A0: forall n : nat, n + 0 = n
H0: x + 0 = x
x + 0 = x
    equals_elim H0.
x: nat
A0: forall n : nat, n + 0 = n
H0: x + 0 = x
x = x
    equals_intro.
Restart.
forall x : nat, x <= x
    intros x.
x: nat
x <= x
    unfold leq.
x: nat
exists z : nat, x + z = x
    exists 0.
x: nat
x + 0 = x
    lia.
Qed.

(*
3.33 (page 94)
*)
Goal forall x y, even(x) -> even(y) -> even(x+y).
forall x y : nat, even x -> even y -> even (x + y)
Proof.
forall x y : nat, even x -> even y -> even (x + y)
    forall_intro x.
x: nat
forall y : nat, even x -> even y -> even (x + y)
    forall_intro y.
x, y: nat
even x -> even y -> even (x + y)
    impl_intro.
x, y: nat
H0: even x
even y -> even (x + y)
    impl_intro.
x, y: nat
H0: even x
H1: even y
even (x + y)
    defn even.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
exists k : nat, x + y = 2 * k
    exists_elim H0 k1.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
exists k : nat, x + y = 2 * k
    exists_elim H1 k2.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
k2: nat
H3: y = 2 * k2
exists k : nat, x + y = 2 * k
    exists_intro (k1+k2).
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
k2: nat
H3: y = 2 * k2
x + y = 2 * (k1 + k2)
    axiom mul_add_distr_l.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
k2: nat
H3: y = 2 * k2
A0: forall n m p : nat, n * (m + p) = n * m + n * p
x + y = 2 * (k1 + k2)
    forall_elim A0 2.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
k2: nat
H3: y = 2 * k2
A0: forall n m p : nat, n * (m + p) = n * m + n * p
H4: forall m p : nat, 2 * (m + p) = 2 * m + 2 * p
x + y = 2 * (k1 + k2)
    forall_elim H4 k1.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
k2: nat
H3: y = 2 * k2
A0: forall n m p : nat, n * (m + p) = n * m + n * p
H4: forall m p : nat, 2 * (m + p) = 2 * m + 2 * p
H5: forall p : nat, 2 * (k1 + p) = 2 * k1 + 2 * p
x + y = 2 * (k1 + k2)
    forall_elim H5 k2.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
k2: nat
H3: y = 2 * k2
A0: forall n m p : nat, n * (m + p) = n * m + n * p
H4: forall m p : nat, 2 * (m + p) = 2 * m + 2 * p
H5: forall p : nat, 2 * (k1 + p) = 2 * k1 + 2 * p
H6: 2 * (k1 + k2) = 2 * k1 + 2 * k2
x + y = 2 * (k1 + k2)
    equals_elim H6.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
k2: nat
H3: y = 2 * k2
A0: forall n m p : nat, n * (m + p) = n * m + n * p
H4: forall m p : nat, 2 * (m + p) = 2 * m + 2 * p
H5: forall p : nat, 2 * (k1 + p) = 2 * k1 + 2 * p
H6: 2 * (k1 + k2) = 2 * k1 + 2 * k2
x + y = 2 * k1 + 2 * k2
    equals_elim_rev H2.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
k2: nat
H3: y = 2 * k2
A0: forall n m p : nat, n * (m + p) = n * m + n * p
H4: forall m p : nat, 2 * (m + p) = 2 * m + 2 * p
H5: forall p : nat, 2 * (k1 + p) = 2 * k1 + 2 * p
H6: 2 * (k1 + k2) = 2 * k1 + 2 * k2
x + y = x + 2 * k2
    equals_elim_rev H3.
x, y: nat
H0: exists k : nat, x = 2 * k
H1: exists k : nat, y = 2 * k
k1: nat
H2: x = 2 * k1
k2: nat
H3: y = 2 * k2
A0: forall n m p : nat, n * (m + p) = n * m + n * p
H4: forall m p : nat, 2 * (m + p) = 2 * m + 2 * p
H5: forall p : nat, 2 * (k1 + p) = 2 * k1 + 2 * p
H6: 2 * (k1 + k2) = 2 * k1 + 2 * k2
x + y = x + y
    equals_intro.
Restart.
forall x y : nat, even x -> even y -> even (x + y)
    intros x y Hx Hy.
x, y: nat
Hx: even x
Hy: even y
even (x + y)
    destruct Hx as [k1 Hk1].
x, y, k1: nat
Hk1: x = 2 * k1
Hy: even y
even (x + y)
    destruct Hy as [k2 Hk2].
x, y, k1: nat
Hk1: x = 2 * k1
k2: nat
Hk2: y = 2 * k2
even (x + y)
    exists (k1+k2).
x, y, k1: nat
Hk1: x = 2 * k1
k2: nat
Hk2: y = 2 * k2
x + y = 2 * (k1 + k2)
    rewrite Hk1, Hk2.
x, y, k1: nat
Hk1: x = 2 * k1
k2: nat
Hk2: y = 2 * k2
2 * k1 + 2 * k2 = 2 * (k1 + k2)
    lia.
Qed.


(*
For more examples see 2022/script.v
*)