All Questions
169
questions
0
votes
1
answer
45
views
How to instruct `auto` to simplify the goal during proof search?
A minimal example of my issue looks as follows:
Goal let x := True in x.
This is immediately solved by simpl. auto., but auto. does not work.
In my actual case, the search tree is a bit bigger than ...
- 6,859
0
votes
1
answer
60
views
Is is possible to rename a coq term?
Sorry, I'm not sure if the title is the adequate question.
I have been going through Logical Foundations. In the Lemma "double_plus" i solved it with this solution:
Lemma double_plus : ...
- 71
0
votes
2
answers
212
views
How to prove that nat_to_bin combines bin_to_nat b = normalize b in Coq
I am a green hand in studying Coq with the reference book softwarefoundation-induction
In the last part of this phrase, there is an exercise about proving that
change a binary to a nature number and ...
0
votes
1
answer
47
views
Is there a way for Coq to recall it already proved a property for the same element in the same proof?
In Coq, I have an inductive property on elements which may appear many times in the same proof. I would like to know if it is possible for Coq to memorize elements for which the property has already ...
- 57
1
vote
1
answer
52
views
Proving n + S n = S (n + n) without n + S m = S (n + m)
Is it possible to prove forall n, n + S n = S (n + n) (with or without induction) without using forall n m, n + S m = S (n + m)?
Looking at the proof, if I start by using induction on n, we end up in ...
0
votes
2
answers
334
views
Lean4: Proving that `(xs = ys) = (reverse xs = reverse ys)`
Intuitively stating that xs is equal to ys is the same as saying that the respective reverse lists are equal to each other.
I'm currently learning Lean 4 and so I set myself the following exercise. I ...
- 253
0
votes
2
answers
152
views
Proof that "if m <= n then max(m, n) = n" in Coq
Yesterday I asked a question here about a proof in Coq and the answer helped me a lot, I was able to solve many exercises alone and discover new features. Today I have another exercise, which states ...
- 5
0
votes
0
answers
198
views
Can someone help me with this proof about the pumping lemma using coq?
This is an exercise from software foundation.
I have proved weak pumping lemma, but I don't know how the prove the strong one.
When I try proving the third case 'App', I can't deal with length (s1 ++ ...
2
votes
1
answer
139
views
I'm trying to build a proof in Coq that two different permutation definitions are equivalent, but the non-inductive side is not working
The two definitions are these:
Inductive perm : list nat -> list nat -> Prop :=
| perm_eq: forall l1, perm l1 l1
| perm_swap: forall x y l1, perm (x :: y :: l1) (y :: x :: l1)
| perm_hd: ...
- 21
3
votes
1
answer
182
views
Coq: Simpl in match pattern when having an inequality hypothesis
I have a definition involving match, similar like this:
Definition five (n: nat): bool :=
match n with
| 5 => true
| _ => false
end.
I try to proof something similar like this:
Theorem fiveT: ...
- 43
1
vote
2
answers
97
views
Coq: Implementation of splitstring and proof that nothing gets deleted
after working for a whole day on this with no success, I might get some help here.
I implemented a splitString function in Coq: It takes a String (In my case a list ascii) and a function f: ascii->...
- 43
1
vote
1
answer
47
views
How do I show that if a hypothesis implies not, it's the same as saying the proposition equals false (coq)?
I want to prove two characters are not equal. My environment currently looks like this:
H: c1 = c2 -> not
_____________________
Goal: (c1 =? c2)%char = false
It won't allow me to apply H or ...
- 11
0
votes
1
answer
175
views
how to code in coq a function that sum the integers represented by the 2 lists and boolean representing a holdback?
I want to set the recursive function badd_r: list bool -> list bool -> bool -> list bool that sum the integers represented by the 2 lists and boolean representing a holdback.
I need to use ...
- 15
0
votes
1
answer
60
views
proving a binary add function
I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).
I have created this badd function that ...
- 15
0
votes
2
answers
129
views
How to do an inductive proof
I have to show that :
Lemma bsuccOK: forall l, value (bsucc l) = S (value l).
with an induction proof, but I don't understand how to do it.
Here is the bsucc function:
Fixpoint bsucc (l: list bool): ...
- 15