Self-evaluation 3

Exercise 1

Write down the induction principle for even.

Inductive even : nat -> Prop :=
| evenO : even 0
| evenS n : even n -> even (S (S n)).

Exercise 2

We give you the definition of disjunction as a reminder.

Inductive or (A B : Prop) : Prop :=
| or_introl : A -> A \/ B
| or_intror : B -> A \/ B.

Notation "A \/ B" := (or A B).

Complete the following definition with a proof term.

#[refine]
Definition or_imp :
  forall (P Q R : Prop), (P -> R) -> (Q -> R) -> P \/ Q -> R
:= _.
forall P Q R : Prop, (P -> R) -> (Q -> R) -> P \/ Q -> R
Proof.
forall P Q R : Prop, (P -> R) -> (Q -> R) -> P \/ Q -> R Admitted.

Exercise 3

What is the goal after the following script?

Lemma true_false :
  true <> false.
true <> false
Proof.
true <> false
  intro e.
e: true = false
False
  change (if true then False else True).
e: true = false
if true then False else True
  rewrite e.
e: true = false
True
  (* HERE *)
Abort.

Exercise 4

Inductive le (n : nat) : nat -> Prop :=
| le_n : n <= n
| le_S : forall m, n <= m -> n <= S m.

What is the goal after the following script?

Lemma le_n_S :
  forall n m,
    n <= m ->
    S n <= S m.
forall n m : nat, n <= m -> S n <= S m
Proof.
forall n m : nat, n <= m -> S n <= S m
  intros n m h.
n, m: nat
h: n <= m
S n <= S m
  induction h as [| m h ih].
n: nat
S n <= S n
n, m: nat
h: n <= m
ih: S n <= S m
S n <= S (S m)
  -
n: nat
S n <= S n constructor.
  - (* HERE *)
n, m: nat
h: n <= m
ih: S n <= S m
S n <= S (S m)
Abort.