CoCalc Public Filescoq.ipynb
Author: Harald Schilly
Views : 81
Compute Environment: Ubuntu 20.04 (Experimental)

COQ in CoCalc

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 [ ]: