Skip to main content

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).

Filter by
Sorted by
Tagged with
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 ...
ice1000's user avatar
  • 6,186
12 votes
1 answer
579 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: ...
march's user avatar
  • 373
11 votes
2 answers
407 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 ...
L. F.'s user avatar
  • 213
10 votes
2 answers
133 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 ...
Bolton Bailey's user avatar
8 votes
2 answers
212 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 ...
CrabMan's user avatar
  • 317
8 votes
1 answer
338 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 ...
Weier's user avatar
  • 313
6 votes
2 answers
397 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 ...
march's user avatar
  • 373
6 votes
1 answer
546 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 ...
uhbif19's user avatar
  • 167
6 votes
1 answer
377 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 ...
Kiran Gopinathan's user avatar
5 votes
1 answer
292 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 ...
Tempestas Ludi's user avatar
5 votes
1 answer
433 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,...
Jeremy Salwen's user avatar
5 votes
1 answer
464 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 ...
Jeremy Salwen's user avatar
5 votes
0 answers
156 views

Prove equality in a record type

I am trying to prove something about monoids an categories. This results in the following (partial) proof: ...
Tempestas Ludi's user avatar
4 votes
1 answer
172 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: ...
q.undertow's user avatar
4 votes
2 answers
183 views

Which proof assistants implement Church's rule?

Church's rule (CR) is one of the hallmarks of constructive mathematics, and is an admissible rule in a wide variety of constructive theories (you might consider CR to be a requirement for constructive ...
Christopher King's user avatar
4 votes
1 answer
1k views

Doing case-by-case proofs about match statements in Lean4

In Lean4, I am stuck in a proof with a goal like this: ...
Jeremy Salwen's user avatar
4 votes
0 answers
61 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 ...
Vladimir Prigodsky's user avatar
3 votes
2 answers
64 views

Creating a tactic for 'destructing' a list by last element?

Sometimes, I have a context in which I have some l : list X, and I want to prove the goal by proving that (1) If l = [], the ...
Agnishom Chattopadhyay's user avatar
3 votes
1 answer
194 views

Selecting both a hypothesis and Goal while applying a tactic

I have a hypothesis H and some function foo. I want to simplify foo in both H and the ...
Agnishom Chattopadhyay's user avatar
3 votes
2 answers
225 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) ...
Malcolm Sharpe's user avatar
3 votes
2 answers
125 views

Lean4: How to construct an HEq between dependent functions?

I have an extremely simple goal to prove: HEq (fun px rd => match px, rd with | Sum.inr _ppos, dir => dir) fun x => id The reason the match ...
André Muricy's user avatar
3 votes
0 answers
87 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?
Jacob woolcutt's user avatar
2 votes
3 answers
195 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)... ...
Agnishom Chattopadhyay's user avatar
2 votes
1 answer
145 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. ...
Åsmund Kløvstad's user avatar
2 votes
1 answer
55 views

What's the idiomatic way to instantiate a tuple of evars in Ltac2?

Suppose that I have a local definition of a type ty in the context, and ty can be any nested tuple, e.g.: ...
Ke Du's user avatar
  • 23
2 votes
1 answer
84 views

What does `induction ... in ...` do in Coq?

I'm self-studying the Semantics course, and met the following proof script in the warmup directory: ...
Jay Lee's user avatar
  • 123
2 votes
1 answer
88 views

Proving that equality is decidable on an ``Inductive Set``

I've managed to prove that equality within a type is indeed decidable. ...
Johan Buret's user avatar
2 votes
1 answer
137 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 ...
8bc3 457f's user avatar
  • 224
1 vote
1 answer
346 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 ...
Greg Nisbet's user avatar
  • 2,771
1 vote
1 answer
114 views

Rewriting inside quantified propositions in Coq?

Is there a simple way to use rewrites inside quantified Props? As an example, consider the following: ...
Agnishom Chattopadhyay's user avatar
1 vote
1 answer
101 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 ...
Trebor's user avatar
  • 3,967
1 vote
1 answer
95 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?
AgentSmith's user avatar
0 votes
1 answer
104 views

Specializing forall quantifiers in Coq

I have an inductively defined type of expressions: ...
Andrii Kozytskyi's user avatar
0 votes
1 answer
35 views

Tactic to Propify a bool expression

Let's say I have bool expressions <bexp> consisting of true, false, variables, ...
Agnishom Chattopadhyay's user avatar
0 votes
1 answer
44 views

Ltac, How to intro a fresh variable which may already have a good estiblished name given by a universal quantifier?

Context I am currently self studying Coq following the Software Foundations book series which I am finding very approachable. I have finally gotten round to ...
user2628206's user avatar