Self-evaluation 1

Exercise 1

In the code below, write down the goal at the annotated points. Goals have the following shape.

h1 : P1
h2 : P2
…
-------------
G

You can ignore the admit below.

Lemma test1 (P Q : Prop) : P \/ Q -> Q \/ P.
P, Q: Prop
P \/ Q -> Q \/ P
Proof.
P, Q: Prop
P \/ Q -> Q \/ P
  intros h.
P, Q: Prop
h: P \/ Q
Q \/ P
  destruct h as [h | h].
P, Q: Prop
h: P
Q \/ P
P, Q: Prop
h: Q
Q \/ P
  -
P, Q: Prop
h: P
Q \/ P left.
P, Q: Prop
h: P
Q
    (* POINT 1 *)
Abort.

Lemma test2 (P Q : Prop) : ~~ P -> (P -> ~ Q) -> ~ Q.
P, Q: Prop
~ ~ P -> (P -> ~ Q) -> ~ Q
Proof.
P, Q: Prop
~ ~ P -> (P -> ~ Q) -> ~ Q
  intros h1 h2 h3.
P, Q: Prop
h1: ~ ~ P
h2: P -> ~ Q
h3: Q
False
  apply h1.
P, Q: Prop
h1: ~ ~ P
h2: P -> ~ Q
h3: Q
~ P intros h4.
P, Q: Prop
h1: ~ ~ P
h2: P -> ~ Q
h3: Q
h4: P
False
  (* POINT 2 *)
Abort.

Lemma test3 (n : nat) : n = 42.
n: nat
n = 42
Proof.
n: nat
n = 42
  induction n as [ | n' IH].
0 = 42
n': nat
IH: n' = 42
S n' = 42
  - (* POINT 3 *)
0 = 42
    admit.
  - (* POINT 4 *)
n': nat
IH: n' = 42
S n' = 42
Abort.

Exercise 2

In the code above, what tactics would solve test2?

Exercise 3

Prove the following lemma without using inversion or discriminate.

Lemma bool_discr : true <> false.
true <> false
Proof.
true <> false
Admitted.