21
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 ...
- 10k
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 ...
- 1,934
9
votes
Accepted
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 <...
- 1,264
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. ...
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 ...
- 1,639
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.
...
- 704
6
votes
Accepted
Applying custom tactic in hypothesis
I believe replacing your definition of unfolds' with
Tactic Notation "unfolds" "in" hyp(H) := ... should ...
- 206
6
votes
Accepted
Cannot discriminate `0 = 1`
UniMath redefines the notation x = y away from Coq's standard eq (without also replacing ...
- 573
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: ...
- 299
5
votes
Accepted
Selecting both a hypothesis and Goal while applying a tactic
You can write simpl in H |- *.
For instance:
...
- 306
5
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:
...
- 226
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 ...
- 5,620
5
votes
Accepted
Form of intros in Coq specifically for `forall` and explicitly for `->`
intros * only unpacks forall. Example from the reference manual:
...
- 2,087
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 ...
- 271
4
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 ...
- 10k
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. ...
- 704
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 ...
- 9,653
4
votes
Accepted
Simple Proof about `String.split`
I personally believe that this is impossible. Note that the signature of splitAux is:
...
- 6,346
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:
...
- 476
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 ...
- 9,653
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. ...
- 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:
...
- 131
3
votes
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
3
votes
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
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 ...
- 10k
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 <...
- 136
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 ...
- 5,620
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:
...
- 226
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 ...
- 5,620
Only top scored, non community-wiki answers of a minimum length are eligible