58 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
0
votes
1
answer
76
views
How to prove if a list `n::l` is an in-order merge of 2 lists `n::l1` `l2`, then `l` is an in-order merge of `l1` and `l2` in Coq?
In IndProp.v of
Logical Foundations,
an exercise is to definde an inductive relation that a list is an in-order merge of
the other 2 lists. I tried to define it as:
Inductive merge {X:Type} : list X -&...
2
votes
1
answer
92
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
72
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))) ->
...
1
vote
1
answer
79
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 ...
0
votes
1
answer
452
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 <=?...
2
votes
3
answers
837
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 ...
3
votes
2
answers
872
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) :...
5
votes
3
answers
521
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 ...
0
votes
1
answer
388
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 ...
2
votes
0
answers
421
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,
...
1
vote
1
answer
61
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 -...
0
votes
2
answers
220
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
250
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 : ...
7
votes
1
answer
925
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:
...
0
votes
1
answer
112
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....