Questions tagged [tactic]
A tactic is a command or instruction for constructing a formal proof by applying a common proof technique. For questions about high-level techniques for constructing proofs, use the tag (strategy).
26
questions
5
votes
1
answer
452
views
Examples of theories where tactic language is required for simple proofs
I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
- 158
7
votes
1
answer
213
views
How does Lean `simp` tactic work?
The doc at https://leanprover-community.github.io/extras/simp.html says about simp:
all it does is repeatedly replace (or rewrite) subterms of the form A by B, for ...
- 273
0
votes
1
answer
68
views
Specializing forall quantifiers in Coq
I have an inductively defined type of expressions:
...
4
votes
0
answers
45
views
Using CoqHammer from Ltac2
As it seems most likely to me, due to the special way arguments are evaluated in CoqHammer tactics (I tried to read the source code in OCaml but unfortunately I didn't understand much of it), it is ...
1
vote
1
answer
84
views
Rewriting inside quantified propositions in Coq?
Is there a simple way to use rewrites inside quantified Props? As an example, consider the following:
...
- 1,241
2
votes
1
answer
75
views
Debug autorewrite in Coq
I often meet proofs using autorewrite which Coq takes a while to process for some reason. (Setoid rewriting)
I then manually figure out which rewrite rules were ...
- 224
1
vote
1
answer
67
views
Question about the tactic "obtain"
I am having difficulty activating the tactic obtain. Is it part of mathlib and where is its exact location?
- 113
2
votes
3
answers
133
views
In Coq, is there a simpler tactic for introducing a disjunction and immediately destructing it?
Very often, I find myself writing some tactics like these:
assert (delta = 1 \/ delta <> 1) as Hd by lia.
destruct Hd.
...(proceed to work with two cases)...
...
- 1,241
4
votes
1
answer
630
views
Doing case-by-case proofs about match statements in Lean4
In Lean4, I am stuck in a proof with a goal like this:
...
- 247
5
votes
1
answer
276
views
Tactics for Array/List simplification in lean4
Because there are both Arrays and Lists in Lean4, sometimes you end up with code that has a mixture of Lists and Arrays interspersed with basic operations and conversions between the two. For example,...
- 247
4
votes
1
answer
353
views
Simple Proof about `String.split`
I am new to lean, working on proving a simple lemma in lean4.
lemma String.split_empty (c): String.split "" c = [""]
I tried looking for ...
- 247
2
votes
1
answer
122
views
Applying custom tactic in hypothesis
To avoid tedious repetition I have a tactic that looks something like this:
Ltac unfolds := try unfold foo;
try unfold bar;
try unfold baz;
apply some_lemma.
...
- 160
1
vote
1
answer
79
views
Proving that applicative functors compose
For simplicity, here an applicative functor means (in a proof assistant based on dependent type theory) the Haskellian applicative functor, bundled with its equational laws.
This I can of course brute ...
- 3,688
3
votes
2
answers
174
views
Coq: can `tauto` be used to prove classical tautologies?
When I experiment, I get inconsistent results.
Running the following code (with a proof included to double-check that it's provable)
...
3
votes
0
answers
77
views
Where is the discriminate tactic defined in Coq?
One can read the Coq documentation about discriminate tactic here.
Were is this tactic actually defined?
5
votes
1
answer
200
views
How to evaluate proof terms through opaque definitions?
Is there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts.
I understand why Coq doesn’t do this by default, and guess it would probably ...
5
votes
0
answers
126
views
Prove equality in a record type
I am trying to prove something about monoids an categories. This results in the following (partial) proof:
...
- 245
4
votes
1
answer
234
views
Cannot discriminate `0 = 1`
I am just practicing a bit with coq, doing some UniMath exercises and am trying to prove (0 = 1) -> empty. However, for some reason, I seem unable to reason ...
- 245
11
votes
2
answers
388
views
Proving uniqueness of an instance of an indexed inductive type
Consider the simple indexed inductive type
Inductive Single : nat -> Set :=
| single_O : Single O
| single_S {n} : Single n -> Single (S n).
Intuitively, I ...
- 213
4
votes
1
answer
170
views
Why does this trivial proof fail with structuring tacticals?
Given this:
Inductive color := Black | White.
Inductive point_state :=
| Occupied of color
| Empty
.
this works:
...
- 143
18
votes
2
answers
1k
views
What's the difference between reflection and tactics?
Agda has a reflection mechanism (not equality reflection or reflexivity, but something related to metaprogramming based on goals and contexts to generate terms) and people have developed some ...
- 5,857
1
vote
1
answer
228
views
Form of intros in Coq specifically for `forall` and explicitly for `->`
Are there tactics in Coq that are more limited versions (subtactics?) of intros?
I'm curious if there are any specifically for ...
- 2,711
6
votes
2
answers
259
views
How do we resolve metavariables that appear in hypotheses and targets in Lean?
There are two related questions that I expound on below. It might seem like these aren't quite related, but they are both about how to deal with meta-variables that appear when working through a ...
- 363
8
votes
2
answers
197
views
How to prove `forall m n : nat, m == n -> m = n`?
I am learning Coq with ssreflect. Just to understand things, I've proved forall a b : bool, a == b -> a = b but I can't figure out how to prove ...
- 317
10
votes
2
answers
124
views
Can Lean simp arguments be ordered?
I want to simplify the expression 0 * 1 * 1 * 1 * 0 using simp only [mul_zero, zero_mul]. I would like ...
- 686
12
votes
1
answer
443
views
In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?
In Lean, when proving basic theorems, one runs into the following kind of thing:
...
- 363