theorem-proving Questions
2
Solved
I try using the syntax for inductive datatypes but it got an error message "mutually inductive types must compile to basic inductive type with dependent elimination".
Below is an example of my att...
Karbala asked 21/1, 2017 at 4:36
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
2
Solved
I'm trying to compile an Agda file, but I'm having trouble getting it to find the standard library. I've seen the documentation here.
I've used Stack to install it:
> which agda
/home/joey/.lo...
Hervey asked 27/10, 2017 at 21:51
3
Solved
I am trying to learn agda. However, I got a problem. All the tutorials which I found on agda wiki are too complex for me and cover different aspects of programming. After parallel reading of 3 tuto...
Skeg asked 26/2, 2012 at 18:20
2
Solved
I am trying to retrieve all possible models for some first-order theory using Z3, an SMT solver developed by Microsoft Research. Here is a minimal working example:
(declare-const f Bool)
(assert (...
Seadon asked 15/11, 2012 at 10:18
2
In Lean I occasionally want to apply a rw tactic to exactly one of multiple identical terms. For example I have the goal
⊢ 0 = 0
and I want to rw it to
⊢ a * 0 = 0
I also have
mul_zero (a : mynat...
Hidie asked 4/10, 2021 at 13:50
1
Solved
I've (mistakenly) picked up a course about verifying concurrent programs, and we've so far covered this method called "Owicki-Gries method". Apparently, one can prove various results about the prog...
Medievalist asked 25/9, 2014 at 5:15
2
I sometimes find it hard to use Isabelle because I cannot have a "print command" like in normal programming.
For example, I want to see what ?thesis. The concrete semantics book says:
The unkno...
Torquemada asked 17/5, 2020 at 20:30
1
I was trying to go through the Isar chapter for Isabelle (theorem Prover) and the first statement has:
lemma "¬ surj(f :: 'a ⇒ 'a set)"
I wanted to understand what the constant surj was. I know ...
Addressee asked 13/5, 2020 at 14:53
1
Solved
I can't tell in which situations I should use Theorem over Lemma or the opposite. Is there any difference (except syntactical) between this
Theorem l : 2 = 2.
trivial.
Qed.
and this
Lemma l : 2 =...
Again asked 9/6, 2019 at 19:30
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
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
1
Solved
Apparently, there is some feature in Agda called positivity checking which can apparently keep the system sound even if type-in-type is enabled.
I am curious to know what this is about, but ...
Hausa asked 9/7, 2018 at 16:45
2
Solved
I was reading Idris tutorial. And I can't understand the following code.
disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p ()
where
disjointTy : Nat -> T...
Unidirectional asked 28/3, 2018 at 7:27
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
1
Solved
I would like to prove properties of expressions involving matrices and vectors (potentially large size, but size is fixed).
For example I want to prove that the outcome of an expression is a diag...
Gearhart asked 7/11, 2017 at 18:56
0
Monadic First Order Logic, where all predicates take exactly one argument, is a known decidable fragment of first order logic. Testing whether a formula is satisfiable in this logic is decidable, a...
Feinberg asked 7/11, 2017 at 6:37
2
Solved
I would like to write a function that takes two natural arguments and returns a maybe of a proof of their equality.
I'm trying with
equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True)
e...
Lipscomb asked 20/10, 2017 at 16:58
1
Solved
I'm trying to understand inductive types from chapter 7 of "theorem proving in lean".
I set myself a task of proving that successor of natural numbers has a substitution property over equality:
i...
Hobart asked 17/7, 2017 at 10:37
3
Solved
Perhaps this is a stupid question. Here's a quote from the Hasochism paper:
One approach to resolving this issue is to encode lemmas, given by
parameterised equations, as Haskell functions. In ...
Photosphere asked 13/5, 2015 at 20:40
1
Solved
Is there a way to admit asserts in Coq ?
Suppose I have a theorem like this:
Theorem test : forall m n : nat,
m * n = n * m.
Proof.
intros n m.
assert (H1: m + m * n = m * S n). { Admitted. }
...
Blackfish asked 14/3, 2017 at 16:28
1
Solved
In Coq, sig is defined as
Inductive sig (A:Type) (P:A -> Prop) : Type :=
exist : forall x:A, P x -> sig P.
Which I read as
"A sig P is a type, where P is a function taking an A and ret...
Nucleon asked 4/1, 2017 at 10:12
1
Solved
I'm going through Terry Tao's real analysis textbook, which builds up fundamental mathematics from the natural numbers up. By formalizing as many of the proofs as possible, I hope to familiarize my...
Aleris asked 16/6, 2016 at 9:35
1
Solved
What is the difference between logic programming and automated theorem proving (ATP) (e.g. with E-Prover, Spass or Princess)?
I searched a lot and the only information I found is that ATP is the p...
Nelle asked 31/3, 2016 at 14:0
1
Solved
is there anything like the tactic simpl for Program Fixpoints?
In particular, how can one proof the following trivial statement?
Program Fixpoint bla (n:nat) {measure n} :=
match n with
| 0 =&g...
Urbanist asked 31/3, 2016 at 9:22
1 Next >
© 2022 - 2024 — McMap. All rights reserved.