Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Examples in Mike Nahas's tutorial

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Examples in Mike Nahas's tutorial


Chronological Thread 
  • From: Hussain Sobhy <hussain.sob7y AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Examples in Mike Nahas's tutorial
  • Date: Wed, 27 Apr 2016 23:08:41 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=hussain.sob7y AT gmail.com; spf=Pass smtp.mailfrom=hussain.sob7y AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f174.google.com
  • Ironport-phdr: 9a23:0sA0jBFh2g4zgcXhl1hMmJ1GYnF86YWxBRYc798ds5kLTJ75o8ywAkXT6L1XgUPTWs2DsrQf27qQ4/urADRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nh6bioNaKO01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y48T34NmxtOSzPC5hHrFsPxrzDhv+t7njKdN5LnZb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf5qg==

Hello,

I was going through Mike Nahas's tutorial (https://coq.inria.fr/tutorial-nahas) and I came across two examples which I can't get working on CoqIde.
Inductive or (A B:Prop) : Prop :=
  | or_introl : A -> A \/ B
  | or_intror : B -> A \/ B
where "A \/ B" := (or A B) : type_scope.

First Example:

Theorem left_or : (forall A B : Prop, A -> A \/ B).
Proof.
  intros A B.
  intros proof_of_A.
  pose (proof_of_A_or_B := or_introl proof_of_A : A \/ B).
  exact proof_of_A_or_B.
Qed.


Error:
In environment
A, B : Prop
proof_of_A : A
The term "proof_of_A" has type "A"
while it is expected to have type
"Prop".


Second Example:

Theorem right_or : (forall A B : Prop, B -> A \/ B).
Proof.
  intros A B.
  intros proof_of_B.
  refine (or_intror _).
    exact proof_of_B.
Qed.


Error:
In environment
A, B : Prop
proof_of_B : B
The term "or_intror ?P" has type
 "forall B0 : Prop, B0 -> ?P \/ B0"
while it is expected to have type
"A \/ B".


Is it due to the fact that the tutorial used an old version of Coq or is there something fundamentally wrong here?

Thanks,
Hussain



Archive powered by MHonArc 2.6.18.

Top of Page