CoCalc Public Filescoq.ipynbOpen with one click!
Author: Harald Schilly
Views : 81
Compute Environment: Ubuntu 20.04 (Experimental)
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.
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.
In [11]:
Theorem implication : forall A B : Prop, A -> (A -> B) -> B .
Proving: implication

1 subgoal

-------------- (1/1)
forall A B : Prop, A -> (A -> B) -> B
Cell evaluated.
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.

Cell evaluated.
In [22]:
Theorem t3 : bool. Proof. pose (b1 := true). pose (b2 := false).
Proving: t3

1 subgoal

b1 := true : bool
b2 := false : bool

-------------- (1/1)
bool
Cell evaluated.
In [23]:
exact b2.
Proving: t3

No more subgoals
Cell evaluated.
In [24]:
Compute match 0 with | 0 => 1 + 1 | S n' => n' end.
     = 2
     : nat

Proving: t3

No more subgoals
Cell evaluated.
In [ ]: