The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

There is much smaller toy example. I have to apologise about not minimizing it previously.
 
 

Let's take a list, that should contain only zeroes.

Inductive list := nil | cons: nat -> list -> list.

Fixpoint no_zeroes (L: list) := match L with nil => True | cons n t => n <> O /\ no_zeroes t end.
 

How to merge both into mutually inductive definitions? Is it possible?
 

Something like

 

Inductive xlist :=

| nil
| cons: nat -> ∀ (L: xlist), no_zeroes L -> xlist

with

no_zeroes := ...

On Mon, Feb 15, 2016 at 7:09 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Here it is:

Inductive list A: nat → Type :=

 | nil: list A 0

 | cons: ∀ n, A → list A n → list A (S n).

Definition Language (A B: Type) := A → nat.

Inductive Term A B (W: Language A B) :=

 | variable: nat → Term W

 | function_node: ∀ x, list (Term W) (W x) → Term W

 | binder_node: ∀ (b: B) (v: nat), Term W → Term W.

 

Here I want to add the following condition in this inductive definition (for binder_node case).
 

Fixpoint variable_is_free A B (W: Language A B) (T: Term W) (x: nat) :=

 match T with

 | variable _ v => True

 | function_node _ L => Forall L (λ t, variable_is_free t x)

 | binder_node _ v t => v <> x ∧ variable_is_free t x

 end.

It should be something similar to this:
 

Inductive Term A B (W: Language A B) :=

 | variable: nat → Term W

 | function_node: ∀ x, list (Term W) (W x) → Term W

 | binder_node: ∀ (b: B) (v: nat) (T: Term W), variable_is_free T v → Term W

with variable_is_free A B (W: Language A B) := ...

 

How can I do such thing?