All Questions
38
questions
1
vote
1
answer
63
views
Recursion and Pattern matching in Coq
I am learning Coq and need to know why the following code does not work in Coq? I am coming from a Haskell background and it is alright there.
Require Import List.
Require Import Bool.
Require Import ...
- 77
0
votes
1
answer
66
views
How does one expand a `fix` function just one step?
I have defined a recursive function with fix, and now I want to prove a rewriting equation about it.
The function in question is a bit big, but here is another function that has the same problem.
(...
- 5,691
0
votes
1
answer
56
views
Two Coq Problems SOS: one is about IndProp, another has something to do with recursion, I guess
(* 4. Let oddn and evenn be the predicates that test whether a given number
is odd or even. Show that the sum of an odd number with an even number is odd. *)
Inductive oddn : nat -> Prop :=
| odd1 ...
- 15
1
vote
3
answers
259
views
How to avoid "Cannot guess decreasing argument of fix." in Coq
(* Define a function sum_digits such that its input is an int， the base of which is b and its
output is the sum of all its digits *)
Definition sum_digits (digits : nat) (base : nat) : nat :=
...
- 15
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
1
vote
1
answer
92
views
How to tell the Coq kernel that a parameter of a lambda function is a subterm of another variable in the scope?
I'm stuck while trying to define a recursive function in Coq over a particular type of n-ary tree.
The n-ary tree type I'm using is defined as a mutually inductive type as follows:
Inductive tree : ...
1
vote
2
answers
181
views
Proving two-list queue in coq
I'm trying to prove correctness of the queue implementation described here:
Inductive queue_type (A : Type) : Type := Queue : list A -> list A -> queue_type A.
Context {A : Type}.
Definition ...
- 3,121
2
votes
1
answer
404
views
Coq Newbie: How to iterate trough binary-tree in Coq
I'm new to coq and need to grab a element that is at a leaf of this binary tree and satisfys P
Variable A : Set.
Variable P : A -> Prop.
Variable P_dec : forall x : A, {P x} + {~ P x}.
Inductive ...
2
votes
3
answers
212
views
How to pattern match exist to transform proofs
I'm messing around with coq and I'm trying to create a function that can be used to lookup something in a list and return an associated proof with it that the specified element is in the list.
In my ...
user2882307
0
votes
1
answer
269
views
Allow potentially infinite loops in Coq
I'm asking your help because I would like to know if it would be possible to allow the definition of potentially infinite fixpoints in Coq, just to check if the current definition eventually produces ...
- 310
0
votes
2
answers
80
views
How does one approach proving facts about non-primitive recursive functions in coq?
I'm trying to prove these two addition functions are extensionally the same, however I can't even prove the simplest lemma for the second one. How does one do this proof over the non-primitive ...
user5775230
2
votes
2
answers
72
views
Proving decidability for a datatype that includes a vector
I'm trying to work with a datatype that represents expressions in a sort of universal algebra context. The usual way to express this in (pen and paper) maths is that you have a set of function symbols,...
- 2,803
2
votes
1
answer
262
views
Recursion for Church encoding of equality
For the Church encoding N of positive integers, one can define a recursion principle nat_rec :
Definition N : Type :=
forall (X:Type), X->(X->X)->X.
Definition nat_rec (z:N)(s:N->N)(n:N) ...
- 1,733
2
votes
1
answer
391
views
Recursion in the calculus of construction
How to define a recursive function in the (pure) calculus of constructions? I do not see any fixpoint combinator there.
- 1,733
2
votes
1
answer
399
views
Can I do “complex” mutual recursion in Coq without let-binding?
Consider the following pair of mutually recursive Coq data types, which represent a Forest of nonempty Trees. Each Branch of a Tree holds an extra boolean flag, which we can extract with isOK.
...
- 36.5k