| Hosted by CoCalc | Download
Kernel: Coq
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.
Cell rolled back. 
Theorem implication :
  forall A B : Prop,
  A ->
  (A -> B) ->
  B
.

Error: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on.
Error while evaluating cell. Cell rolled back. 
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.

Error: No product even after head-reduction.
Error while evaluating cell. Cell rolled back. 
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.
Cell rolled back. 
exact b2.

Proving: t3

No more subgoals
Cell evaluated.
Cell rolled back. 
Compute
    match 0 with
      | 0 => 1 + 1
      | S n' => n'
    end.

     = 2
     : nat

Proving: t3

No more subgoals
Cell evaluated.
Cell rolled back.