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
3 votes
0 answers
55 views

Unfolding expressions in Coq by one layer

Are there any ways to unfold an expression in Coq by a single layer? I have only come up with this obvious solution: ...
user avatar
5 votes
0 answers
86 views

Prove equality in a record type

I am trying to prove something about monoids an categories. This results in the following (partial) proof: ...
user avatar
4 votes
1 answer
154 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 ...
user avatar
11 votes
2 answers
325 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 ...
user avatar
  • 213
4 votes
1 answer
148 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: ...
user avatar
15 votes
2 answers
710 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 ...
user avatar
  • 4,136
1 vote
1 answer
60 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 ...
user avatar
  • 2,467
5 votes
2 answers
91 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 ...
user avatar
  • 333
7 votes
2 answers
137 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 ...
user avatar
  • 273
9 votes
2 answers
96 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 ...
user avatar
11 votes
1 answer
167 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: ...
user avatar
  • 333