The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

Would something like the following suit you ?

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

Fixpoint no_zeroes (L: list) := match L with
  | nil => True
  | cons n t => n <> 0 /\ no_zeroes t
end.
 
Inductive xlist : list -> Prop :=
| xlist_nil
  : (* =============== *)
  xlist nil
| xlist_cons n l
  (XLIST : xlist l)
  (NOZEROS : n <> 0)
  : (* =============== *)
  xlist (cons n l).

Fixpoint In n l := match l with
  | nil => False
  | cons h q => h = n \/ In n q
end.

Fact nonull : forall l, xlist l -> forall v, In v l -> v <> 0.
Proof.
intros.
induction H.
- auto.
- unfold In in H0.
  destruct H0.
  +  subst ; auto.
  + fold In in H0.
    auto.
Qed.

2016-02-16 6:39 GMT+09:00 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?