All Questions
69
questions
0
votes
1
answer
58
views
What `dependent induction` tactic does in Coq and how to use it
Can you please provide me with high-level explanation on which usecases dependent induction / dependent destruct tactics have, and how they work (I would be grateful for explanation high-level enough ...
- 463
0
votes
1
answer
41
views
Coq inductive not right form
I have troubles with a not well formed IH (or I am making mistakes).
From stdpp Require Import mapset.
From stdpp Require Import gmap.
From stdpp Require Import options.
From stdpp Require Import ...
1
vote
2
answers
72
views
Definition by minimization in Coq
Assume P: nat -> T -> Prop is a proposition that for any given t: T,
either there exists a k: nat such that P holds for all numbers greater than or equal to k and no number less than k.
or P k ...
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
97
views
Coq: Implementation of splitstring and proof that nothing gets deleted
after working for a whole day on this with no success, I might get some help here.
I implemented a splitString function in Coq: It takes a String (In my case a list ascii) and a function f: ascii->...
- 43
0
votes
1
answer
65
views
Prove recursive function exists using only `nat_ind`
I'm trying to prove the following in Coq:
∀ B: Type, ∀ a: B, ∀ b: nat -> B -> B, ∃ f: nat -> B, f 0 = a ∧ ∀ n: nat, f (S n) = b n (f n).
Which implies that a fairly general class of ...
- 491
0
votes
1
answer
60
views
proving a binary add function
I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).
I have created this badd function that ...
- 15
0
votes
2
answers
129
views
How to do an inductive proof
I have to show that :
Lemma bsuccOK: forall l, value (bsucc l) = S (value l).
with an induction proof, but I don't understand how to do it.
Here is the bsucc function:
Fixpoint bsucc (l: list bool): ...
- 15
1
vote
1
answer
87
views
How to prove that another definition of permutation is the same as the Default Permutation Library for COQ
I need to proove that a secondary definition of permutation is equivalent to the default definition of permutation in Coq:
Down bellow is the default Permutation definition in Coq
Inductive ...
- 155
3
votes
1
answer
93
views
How to express that one element of an inductive relation can't be derived from another in Coq?
This is slightly different from simple implication, as shown in this toy example.
Inductive R : nat -> nat -> Prop :=
| Base1: R 0 1
| Base2: R 0 2
| Ind: forall n m,
R n m -> R (n+...
0
votes
1
answer
165
views
Coq: Induction on associated variable
I can figure out how to prove my "degree_descent" Theorem below if I really need to:
Variable X : Type.
Variable degree : X -> nat.
Variable P : X -> Prop.
Axiom inductive_by_degree : ...
- 317
1
vote
0
answers
40
views
Coq - trivial induction on lists doesn't accept assumtion
In my current proof, I end up requiring the following result for the else situation of a case disjunction.
1 subgoal (ID 28899)
l : list (Concrete.cvalue sem)
============================
...
- 11
0
votes
1
answer
304
views
Defining integers inductively in Coq (inductive definitions subject to relations)
In Coq, one can define the natural numbers inductively as follows:
Inductive nat :=
| zero : nat
| succ : nat -> nat.
I would like to know if it's possible to define the integers inductively, in a ...
- 909
0
votes
1
answer
56
views
Induction order for relation between three lists
I'm working on a theory of string grammars, but I'm completely blocked by a particular theorem. Every induction ordering I've tried ends up stuck with nonsensical and useless induction hypotheses, and ...
- 2,323
0
votes
1
answer
76
views
Lemma about Sortedness of concatenated lists
I have the following inductive definition for sortedness of a list:
Class DecTotalOrder (A : Type) := {
leb : A -> A -> bool;
leb_total_dec : forall x y, {leb x y}+{leb y x};
leb_antisym :...
