The Coq mailing list

[Gyesik Lee <leegys AT gmail.com>]

Hi,

I am not sure if the title of the message is adequate, so I apologize
in advance for any possible confusion.

========================

(* Consider the following inductive definition.*)

Inductive toto : Type :=
  Var   : toto
| Unit  : toto
| Plus  : toto -> toto -> toto.

(* Now I would like to check if a (t : toto) contains [Var] or not.
One possible definition is as follows *)

Fixpoint VarIn (t:toto) : Prop :=
  match r with
    | Var        => True
    | Unit       => False
    | Plus t0 t1 => (VarIn t0) \/ (VarIn t1)
  end.

(* What I don't like with this definition is that I don't have the
proof unicity without using proof-irrelevance.
This doesn't mean that I don't like proof-irrelevance.

Lemma VarIn_unicity : forall (t : toto) (p q : VarIn t), p = q.

 I am just curious because, on the other hand, the predicate [VarIn]
is decidable, i.e. *)

Lemma VarIn_dec : forall t, {VarIn t} + {~ VarIn t}.
Proof.
  induction t; simpl; firstorder.
Qed.

(* Because of this, I am wondering if a definition like below is
somehow possible:

Fixpoint VarIn (t:toto) : Prop :=
  match r with
    | Var        => True
    | Unit       => False
    | Plus t0 t1 => if {VarIn t0} + {~ VarIn t0} then True else (VarIn t1)
  end.

which would provide me with proof-unicity. So I thought, maybe using
mutual recursion would be possible in the following form:

Fixpoint VarIn (t:toto) : Prop :=
  match t with
    | Var        => _
    | Unit       => _
    | Plus t0 t1 => _
  end

with VarIn_dec (t:toto) : {VarIn t} + {~ VarIn t} :=
  match t with
    | Var        => _
    | Unit       => _
    | Plus t0 t1 => _
  end.

But this is not allowed in Coq. *)

It would be nice if someone tells me if I am trying something possible.

Gyesik