1

In [9]:

Require Import Coq.Logic.JMeq. Inductive Le : nat -> nat -> Set := | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). Parameter P : nat -> nat -> Prop. Goal forall n m:nat, Le (S n) m -> P n m. intros n m H. generalize_eqs H.

2

Proving: Unnamed_thm 1 subgoal n, m, gen_x : nat H : Le gen_x m -------------- (1/1) gen_x = S n -> P n m

Cell evaluated.

Cell rolled back.

In [11]:

Theorem implication : forall A B : Prop, A -> (A -> B) -> B .

3

Proving: implication 1 subgoal -------------- (1/1) forall A B : Prop, A -> (A -> B) -> B

Cell evaluated.

Cell rolled back.

In [18]:

Proof. intros A B. intros proof_of_A. intros A_implies_B. pose (proof_of_B := A_implies_B proof_of_A). exact proof_of_B. Qed.

4

Cell evaluated.

Cell rolled back.

In [22]:

Theorem t3 : bool. Proof. pose (b1 := true). pose (b2 := false).

5

Proving: t3 1 subgoal b1 := true : bool b2 := false : bool -------------- (1/1) bool

Cell evaluated.

Cell rolled back.

In [23]:

exact b2.

6

Proving: t3 No more subgoals

Cell evaluated.

Cell rolled back.

In [24]:

Compute match 0 with | 0 => 1 + 1 | S n' => n' end.

7

= 2 : nat Proving: t3 No more subgoals

Cell evaluated.

Cell rolled back.

In [ ]:

8