All Questions
Tagged with coq logical-foundations
56
questions
2
votes
1
answer
85
views
How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)?
I know how to prove 3 + 2 = 5 using Imp, defined in Software Foundations, Volume 1.
Definition plus2_3_is_5: Prop := forall (st: state),
(X !-> 3) =[ <{ X := X + 2 }> ]=> st -> st X = ...
1
vote
1
answer
43
views
Understanding nat_ind2 in Logical Foundations
As an alternative induction principle of nat, nat_ind2 is defined like so:
Definition nat_ind2 :
forall (P : nat -> Prop),
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S(S n))) ->
...
- 205
1
vote
1
answer
58
views
How do I apply (S n' <=? m) = true to S n' <= m? [closed]
Trying to complete a Coq proof but I ended up getting stuck on the last goal. I transformed the goal to S n' <= m and have a hypothesis (S n' <=? m) = true, but am unable to unify these.
I tried ...
- 15
0
votes
1
answer
201
views
Software Foundations (lf): proving leb_plus_exists and plus_leb_exists
I've been working through Volume 1 of Software Foundations, and I can't get past a pair of optional questions in Logic.v. Anyone have any idea what to do?
Theorem leb_plus_exists : forall n m, n <=?...
- 15
1
vote
2
answers
394
views
Software Foundations Basics - Theorem lower_grade_lowers need to prove implication Eq = Lt -> Eq = Lt
I'm working through Software Foundations on my own and am stuck on the final bullet for lower_grade_lowers. My theorem follows the hint pretty well until that final case which is obviously the crux of ...
- 21
3
votes
2
answers
461
views
Software Foundations Basics Exercise - How do I access letter from grade?
I am working through Software Foundations by myself and am trying the exercises, but I am stuck on the exercise for writing the function grade_comparison.
Definition grade_comparison (g1 g2 : grade) :...
- 33
1
vote
1
answer
305
views
I have been stuck on MApp for pumping lemma
I have been trying to solve Pumping lemma in Coq.
I was on the third subgoal, Mapp.
Lemma pumping : forall T (re : reg_exp T) s,
s =~ re ->
pumping_constant re <= length s ->
exists s1 ...
- 11
0
votes
1
answer
229
views
Cannot focus on a remaining unfocused goal in Coq
I am trying to prove the pumping Lemma (which is one of the exercises of the Logical Foundations book). I thought I had completed the MStarApp case but the interpreter tells me that there are still ...
- 77
0
votes
0
answers
308
views
Stuck at the MApp case in Logical Foundation's pumping lemma
I am teaching myself to use the Coq proof assistant through the Logical Foundations course.
I am stuck trying to prove the MApp case of the pumping lemma.
Lemma pumping : forall T (re : reg_exp T) s,
...
- 77
1
vote
1
answer
47
views
Check cnat. and got Type return
All
I am trying to understand the Church numerals, mentioned in the SF-LF book, chp4.
Definition cnat := forall X : Type, (X -> X) -> X -> X.
Definition one : cnat :=
fun (X : Type) (f : X -...
- 121
0
votes
1
answer
164
views
How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?
I am currently confused about how to prove the following theorem:
Theorem excluded_middle2 :
(forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P).
I am stuck here:
Theorem ...
1
vote
1
answer
183
views
Proving MStar' in Logical Foundations (IndProp.v)
In Logical Foundations' chapter on Inductive Propositions, the exercise exp_match_ex1 involves the following definitions:
Inductive reg_exp (T : Type) : Type :=
| EmptySet
| EmptyStr
| Char (t : ...
- 77
6
votes
1
answer
654
views
How can I prove `add_le_cases` (`forall n m p q, n + m <= p + q -> n <= p \/ m <= q`)
I am trying to complete the series of exercises le_exercises from Logical Foundations' chapter on inductive propositions.
This series is mostly based on the inductive relation le, defined thusly:
...
- 77
0
votes
1
answer
71
views
Mix-up of bool and Datatypes.bool after Require Import coq libraries
2
I'm going through software foundations and ran into an error.
(https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html)
From Coq Require Import Arith.Arith.
From Coq Require Import Bool.Bool....
- 331
0
votes
1
answer
57
views
Coq proving nonsensical inductive property implication?
In IndProp.v from Logical Foundations we have the following inductive property:
Inductive nostutter {X:Type} : list X -> Prop :=
| nos_nil : nostutter []
| nos_one : forall x, nostutter [x]
| ...
- 65