All Questions
Tagged with coq coq-tactic
390
questions
0
votes
0
answers
27
views
Applying lemma using Vectors in Coq
I have proved the following
Lemma exists_distribution:
forall (a:Prop)(Omega:Set)(p:Omega->Prop),
(exists x:Omega, p x->a)<->
((exists x:Omega,~(p x))\/(exists x:Omega,a)).
Now I would ...
- 21
1
vote
0
answers
40
views
How to match implication without prior intros?
I am trying to write a tactic to check if my goal is an implication without having to introduce anything beforehand.
Furthermore I would like this tactic to be compatible with any amount of variables ...
- 21
0
votes
2
answers
72
views
How can I prove that theorem in coq: (x | a) -> (x | b) -> x <= (gcd a b)?
I have this realization of greatest common divisor:
Fixpoint gcd_ (m n d : nat) : nat :=
match d with
| 0 => if (m =? 0) then n else m
| S k => if (m mod S k =? 0) && (n mod S k =? 0) ...
0
votes
1
answer
117
views
Error: Cannot find a physical path bound to logical path Strands. in coq
I have coq file and was working on it for days but now the file giving me following error:
Error: Cannot find a physical path bound to logical path Strands.
also the required packages are as under:
...
- 11
0
votes
1
answer
61
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
-1
votes
1
answer
44
views
Syntax of the case tactic in coq
Can someone explain to me what the following coq tactic is doing?
case x : fun H => [|[]] // _.
How would I rewrite this using destruct?
Even better, can anyone point me to somewhere in the coq ...
- 201
0
votes
1
answer
58
views
What `dependent induction` tactic does in Coq and how to use it
Can you please provide me with high-level explanation on which usecases dependent induction / dependent destruct tactics have, and how they work (I would be grateful for explanation high-level enough ...
- 463
0
votes
2
answers
63
views
Split multiple conjuncts in the goal
Is there a tactic to split multiple conjuncts in a goal into subgoals?
If I have the goal P /\ Q /\ R, I want to split it to produce three subgoals at once:
P, Q, and R
I can't seem to find any info ...
- 205
0
votes
2
answers
84
views
Multiple Assignements in a Coq Map to the same value
I'm given the following definition of com that sssigns new values to more than one variable in a single command.:
Inductive com : Type :=
| CSkip
| CAsgn (xs : list string) (es : list aexp) (* <...
1
vote
2
answers
145
views
How to prove the goals in more elegant way using ssreflect?
It seems my coq proofs are longer and uglier than expected and I can't achieve ssreflect advantages in them despite my attempts. I think I missed some key points. Or maybe I just need to know more ...
- 13
0
votes
1
answer
102
views
How to continue case analysis of a nested match in coq?
I recently got a goal from coq (Actually I get this goal from case analysis):
1 goal (ID 110)
addr : nat
x : State
l : list nat
Heqo : write_list_index (repeat 0 (addr + 1)) addr 0 = Some l
...
- 7
0
votes
3
answers
182
views
Why is `specialize` not an invalid tactic within a proof?
In the software foundations book (archived) the specialize tactic was introduced as a way to simplify a hypothesis.
I don't understand,why it's a valid step within a proof.
The provided example adds ...
- 1,324
1
vote
1
answer
36
views
Custom tactics provided by libraries
Is there a way to see all custom tactics provided by a library from inside Coq?
Searching for them using Search does not work.
- 69
0
votes
2
answers
61
views
Is there a three-valued case analysis on patterns (a < b) (a = b) (a > b)?
I want my students to prove some stuff overs Binary Search Trees.
Most of the proofs require to perform a case analysis on some arithmetic inequality over three cases:
a < b (recursive call in the ...
- 1,576
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