coq-tactic Questions
3
I am working on the proof of the following theorem Sn_le_Sm__n_le_m in IndProp.v of Software Foundations (Vol 1: Logical Foundations).
Theorem Sn_le_Sm__n_le_m : ∀n m,
S n ≤ S m → n ≤ m.
Proof.
...
Thill asked 24/5, 2019 at 12:12
1
Solved
I've been working on a formalization for a process calculus in Coq (repository here), and constantly find myself trying to apply a function which fails because of equivalent, but syntactically diff...
Auriferous asked 17/9, 2021 at 20:20
2
Solved
Is it possible to switch the current goal or subgoal to prove in Coq?
For example, I have a goal like this (from an eexists):
______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s...
Anosmia asked 22/12, 2015 at 17:10
2
Solved
Coq simpl / unfold only once. (Replace part of goal with the result of one iteration of a function.)
I am an instructor at university for a class titled Type Systems of Languages and the professor used the following example for inductive proofs in Type Theory on the board last lecture:
Suppose, t...
Breaker asked 16/9, 2019 at 15:6
1
Solved
I find myself often wanting to refer to hypotheses by their type rather than by their name; especially in proofs with inversions on semantic rules, i.e., rules with several cases each of which may ...
Jephum asked 5/5, 2019 at 13:42
2
I was trying to go through the famous and wonderful software foundations book but I got to an example where simpl. and reflexivity. just do to much under the covers and are hindering my learning &a...
Gastrotomy asked 5/1, 2019 at 0:12
3
Solved
I am trying to prove the following lemma in Coq:
Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
(a <> [] \/ b <> []) -> a ++ b...
Repatriate asked 20/11, 2018 at 0:48
0
When writing highly automated proofs in Coq (CPDT-style) proofs, building on extensive use of eauto N, I must often modify my lemma statements to allow eauto to use them easily. In particular, I mu...
Chrisman asked 20/10, 2018 at 16:59
2
Solved
I have a question similar to Decomposing equality of constructors coq, however, my equality contains a match expression. Consider the example (which is nonsensical, but just used for clarification)...
Bac asked 1/5, 2018 at 14:4
1
Solved
In the Coq tactics language, what is the difference between
intro
and
intros?
Tarpon asked 26/4, 2018 at 1:4
1
Solved
Is there any way to use the decide equality tactic with mutually recursive types in Coq?
For example, if I've got something like this:
Inductive LTree : Set :=
| LNil
| LNode (x: LTree) (y: RTr...
Salverform asked 15/1, 2018 at 18:40
2
Solved
I have a string a and on comparison with string b, if equals has an string c, else has string x. I know in the hypothesis that fun x <= fun c. How do I prove this below statement? fun is some fu...
Altocumulus asked 26/9, 2017 at 19:37
3
Solved
How can I invoke rewrite in ltac to only rewrite one occurrence? I think coq's documentation mentions something about rewrite at but I haven't been able to actually use it in practice and there are...
Haleyhalf asked 1/8, 2017 at 2:8
2
Solved
When implementing a complex tactic in Ltac, there are some Ltac commands or tactic invocation that I expect to fail and where that is expected (e.g. to terminate a repeat, or to cause backtracking)...
Extrovert asked 14/7, 2017 at 17:56
2
Solved
Consider the following development:
Require Import Relation RelationClasses.
Set Implicit Arguments.
CoInductive stream (A : Type) : Type :=
| scons : A -> stream A -> stream A.
CoInducti...
Acetylide asked 17/7, 2017 at 18:34
2
Solved
I've come up with the following toy proof script:
Inductive myType : Type :=
| c : unit -> myType.
Inductive myProp : myType -> Type :=
| d : forall t, myProp (c t).
Hint Constructors myPro...
Obscuration asked 26/6, 2017 at 19:59
2
Solved
I was curious about how the discriminate tactic works behind the curtain. Therefore I did some experiments.
First a simple Inductive definition:
Inductive AB:=A|B.
Then a simple lemma which can...
Onehorse asked 23/3, 2017 at 4:42
1
Solved
I have the following Lemma with an incomplete proof:
Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
intros.
reflexivity.
Qed.
This proof fails with
Unable to unify "n + 1" wit...
Caylacaylor asked 28/10, 2016 at 21:55
2
Solved
I read that the induction principle for a type is just a theorem about a proposition P. So I constructed an induction principle for List based on the right (or reverse) list constructor .
Definit...
Dealt asked 12/10, 2015 at 1:18
2
Solved
From the Coq reference manual (8.5p1), my impression is that revert is the inverse of intro, but so is generalize to a certain extent. For example, revert and generalize dependent below seem to be ...
Broad asked 28/6, 2016 at 4:45
2
Solved
Often in Coq I find myself doing the following: I have the proof goal, for example:
some_constructor a c d = some_constructor b c d
And I really only need to prove a = b because everything else ...
Rayshell asked 27/5, 2016 at 19:22
3
Solved
This seems like a really simple question, but I wasn't able to find anything useful.
I have the statement
n - x = n
and would like to prove
(n - x) + x = n + x
I haven't been able to find wh...
Bimolecular asked 3/5, 2016 at 5:38
1
Given a valid Coq proof using the ; tactical, is there a general formula for converting it to a valid equivalent proof with . substituted for ;?
Many Coq proofs use the ; or tactic sequencing tact...
Hindquarter asked 29/3, 2016 at 18:42
3
Solved
I was wondering if there is a way to introduce an entirely new variable during the proof of a theorem in Coq?
For a complete example, consider the following property from here about the evenness of...
Hatshepsut asked 8/10, 2015 at 1:44
1
Solved
I was trying to prove the following simple theorem from an online course that excluded middle is irrefutable, but got stuck pretty much at step 1:
Theorem excluded_middle_irrefutable: forall (P:Pr...
Judie asked 27/9, 2015 at 21:5
1 Next >
© 2022 - 2024 — McMap. All rights reserved.