All Questions
71
questions
1
vote
1
answer
52
views
Proving n + S n = S (n + n) without n + S m = S (n + m)
Is it possible to prove forall n, n + S n = S (n + n) (with or without induction) without using forall n m, n + S m = S (n + m)?
Looking at the proof, if I start by using induction on n, we end up in ...
0
votes
1
answer
195
views
How to prove A \/ False -> A in Coq?
I am learning Coq and trying to prove "A \/ False -> A" but I am not sure what am I doing wrong.
I tried the following code:
Goal forall A False : Prop, A \/ False -> A.
Proof.
...
0
votes
2
answers
334
views
Lean4: Proving that `(xs = ys) = (reverse xs = reverse ys)`
Intuitively stating that xs is equal to ys is the same as saying that the respective reverse lists are equal to each other.
I'm currently learning Lean 4 and so I set myself the following exercise. I ...
- 253
3
votes
1
answer
239
views
Is it possible to convert all higher-order logic and dependent type in Lean/Isabelle/Coq into first-order logic?
More specially, given arbitrary Lean proof/theorem, is it possible to express it solely using first-order logic? If so, is it practical, i.e. the generated FOL will not be enormously large?
I have ...
- 17.2k
2
votes
1
answer
139
views
I'm trying to build a proof in Coq that two different permutation definitions are equivalent, but the non-inductive side is not working
The two definitions are these:
Inductive perm : list nat -> list nat -> Prop :=
| perm_eq: forall l1, perm l1 l1
| perm_swap: forall x y l1, perm (x :: y :: l1) (y :: x :: l1)
| perm_hd: ...
- 21
1
vote
2
answers
382
views
How to prove insert_BST in Coq
I want to prove that when receiving a binary search tree as an argument, the [insert] function generates another binary search tree.
Insert Function:
Fixpoint insert {V : Type} (x : key) (v : V) (t : ...
- 155
0
votes
0
answers
116
views
How to build a proof of correctness in coq for elements_tr
I want to build a proof of correctness for elements_tr...
It is actually related to some sort of reimplementation of BSTs with int keys.
Elements_tr is defined as follows:
Fixpoint elements_aux {V : ...
- 155
0
votes
1
answer
362
views
How to prove in Coq ~~(P \/ ~P)
I want to prove ~~(P \/ ~P) in Coq, which sounds somehow trivial... However I do not know where to go since there is not any single hypothesis.
I have written the following code which is not working, ...
- 155
0
votes
2
answers
646
views
How to prove (~Q -> ~P) - > (P -> Q) in Coq
I am trying to prove (~Q -> ~P) - > (P -> Q) in coq, which is the reverse of the contrapositive theorem (P-> Q) (~Q -> ~P). Currently I was thinking about using the same logic of ...
- 15
-1
votes
1
answer
64
views
Coq begginer here, how to understand the syntax?
I recently started a class on my college where we solve logical problems in Coq. I'm having problems understanding the principles of programming in Coq, the syntax and "building" ideas in my ...
- 1
1
vote
1
answer
72
views
Coq syntax. Predicate Logic
Can anyone help me out with the coq syntax for the following proof:
~ (exists x:D, ~ R x) |- (forall y:D, R y)
- 11
0
votes
1
answer
212
views
Predicate Logic in Coq [closed]
Can anyone help with these two theorems in regards to predicate logic and using coq. I have trouble understanding coq syntax.
exists x:D, (R x /\ S x) |- (exists y:D, R y) /\ (exists z:D, S z)
...
- 11
0
votes
1
answer
257
views
Apply a lemma to a conjunction branch without splitting in coq
I have a conjunction, let's abstract it as: A /\ B and I have a Lemma proven that C -> A and I wish to get as a result the goal C /\ B. Is this possible?
If yes, I'd be interested in how to do it. ...
- 1,014
0
votes
2
answers
166
views
How to model/formalize the change of the variable (change of world) in Isabelle/HOL?
I am trying to formalize business rules in Isabelle/HOL, but business rules involve the change of the values of some variables, like if x=5 => x=6. => is not the usual implication there, because ...
- 2,926
2
votes
1
answer
355
views
How in coq to use lemma a=b backwards?
Suppose I have a lemma L that says
forall x, x + 1 + 1 = x + 2.
If my goal is of the form a + 1 + 1 = b
I can write a command rewrite L to get a goal of the form a + 2 = b
However, if my goal is ...
- 1,439