# Tag Info

Accepted

### What's the difference between reflection and tactics?

Consider a reasonable type theory $T$ with decidable checking. Think of it as the core type theory implemented in the kernel of a proof assistant, i.e., with fully elaborated and annotated judgements ...
• 10k
Accepted

### In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?

My take on that is that, in their first approximation, tactics are just ways to build terms (typically proof terms), so it is expected to have basic tactics that closely correspond to the various term ...
• 1,934
Accepted

### Can Lean simp arguments be ordered?

Using mathlib's simp_rw, you can order your lemmas: ...

### Proving uniqueness of an instance of an indexed inductive type

Or, what would a better way to prove s = single_O? I would define a function that, given a nat n, computes the canonical proof <...
• 1,264
Accepted

### Why does this trivial proof fail with structuring tacticals?

If you look at the documentation of first, first [ tac ] will apply tac to all subgoals. ...

### How do we resolve metavariables that appear in hypotheses and targets in Lean?

Arguably, the most direct way (type theoretically or tactically) to do this is to find the goal that corresponds to ?m_1 and fill it. In your example, the goals ...
• 1,639

### What's the difference between reflection and tactics?

For what I see reflection and tactics live on different planes: (elaborator) reflection is a lower-level mechanism that opens up a possibility to implement all sorts of things, in particular tactics. ...
Accepted

### Applying custom tactic in hypothesis

I believe replacing your definition of unfolds' with Tactic Notation "unfolds" "in" hyp(H) := ... should ...
• 206
Accepted

### Cannot discriminate 0 = 1

UniMath redefines the notation x = y away from Coq's standard eq (without also replacing ...
• 573
Accepted

### How to prove forall m n : nat, m == n -> m = n?

Induction can be used via elim tactic on both m and n, like this: ...
• 299
Accepted

### Selecting both a hypothesis and Goal while applying a tactic

You can write simpl in H |- *. For instance: ...

### In Coq, is there a simpler tactic for introducing a disjunction and immediately destructing it?

You can destruct things in many ways at the time you introduce them with "intro patterns". https://coq.inria.fr/refman/proof-engine/tactics.html#intro-patterns Here are small examples: ...
• 226
Accepted

### Proving uniqueness of an instance of an indexed inductive type

Rergarding IDProp, this is the pattern-matching compilation of Coq at work. Basically, because you scrutinee has a type that can only correspond to the ...
• 5,620
Accepted

### Form of intros in Coq specifically for forall and explicitly for ->

intros * only unpacks forall. Example from the reference manual: ...
• 2,087

### How to prove forall m n : nat, m == n -> m = n?

SSReflect builds upon the relationship between booleans (m == n) and proposition (m = n); this is called reflection, hence the ...

### Which proof assistants implement Church's rule?

Not the answer you would like to hear, but that would be "no proof assistant" (to my knowledge). The first reason is that Church's rule does not hold for classical theories but the ...
• 10k

### Examples of theories where tactic language is required for simple proofs

so far I do not see any reasons why the same reasoning would not work for the rest of SF Wait for (or jump straight to) at least https://softwarefoundations.cis.upenn.edu/slf-current/Rules.html ;) 3. ...
Accepted

### Tactics for Array/List simplification in lean4

Many of the tools for working with programming-like objects (Arrays and such) can be found in either core Lean (Init which is ...
• 9,653
Accepted

### Simple Proof about String.split

I personally believe that this is impossible. Note that the signature of splitAux is: ...
• 6,346

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

A fun way is to express the destructuring as something resembling an induction principle. For example, you can define "snoc induction" like this: ...
• 476
Accepted

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

Note, this my not be the most optimal answer, but here is how I would approach this. Also, note, it is important to provide a MWE when you ask questions like this so that the answerer can plug this ...
• 9,653

### How does Lean simp tactic work?

simp is using discrimination tree to find a small(ish) set of theorems that could be used for a rewrite at a particular place of the expression. ...
• 221

### How do we resolve metavariables that appear in hypotheses and targets in Lean?

It's possible to write a tactic that will assign to meta-variables. This tactic is incomplete but works in your example: ...

### When is the lean 4 "by" required?

by is always required to use tactics. However, there exists some syntactic constructions that have the same name as tactics. ...
• 186
Accepted

### Feeding rewrites and other hints into an omnibus tactic

To use rewriting hints from a hint database, you should use autorewrite (probably with the with keyword to pick a database). ...
• 5,620

### Coq: can tauto be used to prove classical tautologies?

There is a difference between trying to prove forall P, P \/ ~ P and trying to prove P \/ ~P where ...
• 10k
Accepted

### Coq: can tauto be used to prove classical tautologies?

From looking at the Ltac code (https://github.com/coq/coq/blob/d0ed66ddfaa765ad0d9185dd00b68b2fa83cd798/theories/Init/Tauto.v#L97) it seems that tauto in fact has <...
• 136
Accepted

### Specializing forall quantifiers in Coq

The issue comes from your definition of semi-ring morphism. It does not say that a semi-ring homomorphism preserves addition, but rather that there exists some unspecified ...
• 5,620
Accepted

### Rewriting inside quantified propositions in Coq?

Yes, the tactic setoid_rewrite lets you rewrite under binders. Here is the reference manual link. For your example this gives: ...
• 226