Skip to main content
19 votes
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 ...
Andrej Bauer's user avatar
  • 9,104
15 votes
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 ...
Joachim Breitner's user avatar
9 votes
Accepted

Can Lean simp arguments be ordered?

Using mathlib's simp_rw, you can order your lemmas: ...
Yakov Pechersky's user avatar
8 votes

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 <...
gallais's user avatar
  • 1,126
7 votes
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. ...
Théo Winterhalter's user avatar
6 votes

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 ...
Mario Carneiro's user avatar
6 votes

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. ...
Alex Chichigin's user avatar
6 votes
Accepted

Cannot discriminate `0 = 1`

UniMath redefines the notation x = y away from Coq's standard eq (without also replacing ...
HTNW's user avatar
  • 533
5 votes
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: ...
Ihar Bury's user avatar
  • 299
5 votes
Accepted

Selecting both a hypothesis and Goal while applying a tactic

You can write simpl in H |- *. For instance: ...
Yannick Zakowski's user avatar
5 votes
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 ...
Meven Lennon-Bertrand's user avatar
5 votes
Accepted

Applying custom tactic in hypothesis

I believe replacing your definition of unfolds' with Tactic Notation "unfolds" "in" hyp(H) := ... should ...
Rincewind's user avatar
5 votes
Accepted

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

intros * only unpacks forall. Example from the reference manual: ...
Li-yao Xia's user avatar
  • 1,757
4 votes

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 ...
Pierre Jouvelot's user avatar
4 votes

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. ...
Alex Chichigin's user avatar
4 votes
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 ...
Jason Rute's user avatar
  • 8,655
4 votes
Accepted

Simple Proof about `String.split`

I personally believe that this is impossible. Note that the signature of splitAux is: ...
ice1000's user avatar
  • 6,176
4 votes

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: ...
Villetaneuse's user avatar
4 votes

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: ...
JoJoModding's user avatar
3 votes

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 ...
Andrej Bauer's user avatar
  • 9,104
3 votes
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 ...
Jason Rute's user avatar
  • 8,655
3 votes

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. ...
tom's user avatar
  • 221
3 votes

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: ...
Etienne Laurin's user avatar
2 votes

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 ...
Andrej Bauer's user avatar
  • 9,104
2 votes
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 <...
corwin.amber's user avatar
2 votes
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 ...
Meven Lennon-Bertrand's user avatar
2 votes
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: ...
Villetaneuse's user avatar
2 votes
Accepted

Which proof assistants implement Church's rule?

You might want to give a look at A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus by Yannick Forster and Fabian Kuntze. They define a set-up in Coq where using ...
Meven Lennon-Bertrand's user avatar
2 votes

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

Here is a solution that feels more like destruct than induction: ...
Meven Lennon-Bertrand's user avatar
1 vote

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

Since you're dealing with natural numbers, you can also use booleans instead of properties. Using ssreflect, you could then do: ...
Pierre Jouvelot's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible