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
1 vote
1 answer

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 ...
  • 2,916
3 votes
2 answers

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

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

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 ...
4 votes
0 answers

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: ...
5 votes
0 answers

Prove equality in a record type

I am trying to prove something about monoids an categories. This results in the following (partial) proof: ...
4 votes
1 answer

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 ...
11 votes
2 answers

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

Why does this trivial proof fail with structuring tacticals?

Given this: Inductive color := Black | White. Inductive point_state := | Occupied of color | Empty . this works: ...
15 votes
2 answers

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 ...
  • 4,740
1 vote
1 answer

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,593
6 votes
2 answers

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

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

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 ...
12 votes
1 answer

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