Questions tagged [coq-tactic]
Tactics are programs written in Ltac, the untyped language used in the Coq proof assistant to transform goals and terms. This tag should be used on questions related to the issues in using Coq tactics to derive proofs using the Coq proof assistant.
coq-tactic
397
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