The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Fri, 20 Jan 2012 13:55:22 -0800,
Daniel Schepler 
<dschepler AT gmail.com>
 a écrit :

> Actually, I guess that also gives an example of a positive, but not
> strictly positive, inductive definition which would lead to a
> contradiction:
> 
> Inductive X : Type :=
> | X_const : ((X->Prop)->Prop) -> X.
> 
> If Coq allowed that definition, then X_const, being a constructor,
> would automatically be injective, leading to the contradiction from
> my previous message.  (Plus, I'm not at all sure what X_rect or X_ind
> would look like in that case.)

I was able to do your proof (I don't examine the following mail you
wrote, but I guess it is pretty much the same proof).

But I still think that positivity may be relaxed to allow replacement
with elimination principle of inductive types. I think these
elimination principle have some particular patterns; so maybe that
rules like:

| <Constructor_name> :
 (forall (T:X -> Type), (forall u11..u1n, Y1 -> T (f1 u11..u1n)) -> ..
                     -> (forall um1..umn, Ym -> T (fm um1..umn)) ->
                     forall x, T x)
 -> <Inductive_type>

could be allowed, where <Inductive_type> may appear positively (not
necessarily strictly). I am not sure it would be that useful, so it was
the aim of my first question.

Is what I said too complex to formalize and not enough useful to be
implemented?
Is there some case where putting an elimination principle instead of
the inductive can lead to inconsistency?

✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ 

Axiom X : Type.

Axiom X_const : ((X->Prop)->Prop) -> X.

Axiom X_rect : forall (T:X->Type), (forall f:(X->Prop)->Prop, T
(X_const f)) -> forall x, T x.
(*What I would expect for the record*)

Axiom X_const_inj : forall f (P:X->Prop) (Q:((X->Prop)->Prop)->Prop),
                    forall f', (P (X_const f) -> P (X_const f')) ->
                    Q f -> Q f'.

Lemma X_const_injective: forall f1 f2, X_const f1 = X_const f2 -> f1 =
f2. Proof.
 intros.
 eapply X_const_inj; intros.
 eexact H.
 esplit.
Qed.

Lemma eq_inj: forall T (x y:T), eq x = eq y -> x = y.
Proof.
 intros.
 rewrite H.
 split.
Qed.

Goal False.
 set (g := fun h => X_const (eq h)).
 assert (forall h i, g h = g i -> h = i).
  subst g; simpl.
  intros.
  generalize (X_const_injective _ _ H); clear H.
  apply eq_inj.
 set (S0 := fun (x:X) => exists S, g S = x /\ ~ (S x)).
 assert (S0 (g S0) -> False).
  intros L.
  assert (M := L).
  destruct M as [S [K1 K2]].
  assert (Heq := H _ _ K1); clear K1.
  subst; auto.
 apply H0.
 exists S0; auto.
Qed.