A not so FSet specific question about destruction

[Thomas Braibant-2]

Hi list,

This is not a FSet specific questions, more a design question for a
library. Any comment would be appreciated.

Using FSets, consider the following (simplified) goal:
<---
Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1 else 2)= 1.
-->

It can be solved, using by doing a case elimination on the result of
mem ...But relying on case_eq can become tedious, if there are several
such destruction to do. Moreover, you need fruther work if you want to
transform this information (mem x s= true) into something more
"useful" (like In x s).

Moreover, you really want the result of mem to be a boolean, if you
want to build effective functions inside coq, and you can't ask to
have mem of type [ x : elt -> s : t -> {In x s} + {~In x s}, which
would be more informative, I think.

Therefore, I came up with the following scheme of specifications,
<---
Lemma mem_spec : forall x s, {In x s} + {~ In x s}. (* Proofs omitted
*) Admitted.
Lemma mem_proj : forall x s, mem x s = proj_sumbool (mem_dec x s). (*
Proofs omitted *) Admitted.
-->
and I ended up with automation tactics trying to rewrite this kind of
lemma wherever they could, and destroying the resulting *_spec lemmas
(which can be arbitrarily informative, like one would write when
defining strongly specified functions)

I was then told that I could use inductives, to do the same job.
<--
Inductive mem_spec_ind : elt -> t -> bool -> Type :=
    | mem_spec_1 : forall x s, In x s -> mem_spec_ind x s true
    | mem_spec_2 : forall x s, ~In x s -> mem_spec_ind x s false.
Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.
-->

Unfortunately, "destruct"-ing mem_eq in a Goal can lead to the
forgetting of useful informations. I have to remember some pieces of
information by hand, while everything is smoother using the
rewrite-destruct scheme.

The goal here would be to be able to automatize such destructions, in
order to be able to reason more easily on more complicated programs. I
wonder if any function should have such a specification (like add,
below).
Inductive add_spec : elt -> t -> t -> Type :=
| add_spec_1 : forall x s s', (forall y, In y s' <-> (E.eq x y \/ In y
s)) -> add_spec x s s'.
Lemma add_eq : forall x s, add_spec x s (add x s).

Any comment would be appreciated.
Best regards,
Thomas Braibant




<-------------------------------- Complete script
--------------------------------------->
Module Test (X : FSetInterface.S).
  Module OrdProps := FSetProperties.OrdProperties X.
  Module EqProps := FSetEqProperties.EqProperties X.
  Module Props := EqProps.MP.
  Module Facts  := Props.FM.
  Module Dec := Props.Dec.

  Include Facts.
  Include OrdProps.
  Import  X.
  Ltac setdec := Dec.fsetdec.

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
    intros.
    case_eq (mem z (add x (add y (singleton z)))); intro H.
      reflexivity.
      apply False_ind. revert H. rewrite <- not_mem_iff. set_iff. intuition.
  Qed.
  Lemma mem_dec : forall x s, {In x s} + {~ In x s}. Admitted.
  Lemma mem_proj : forall x s, mem x s = proj_sumbool (mem_dec x s).  Admitted.

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
    intros.
    rewrite mem_proj. destruct mem_dec. reflexivity.
    apply False_ind. apply n. set_iff. intuition.
  Qed.

  Inductive mem_spec_ind : elt -> t -> bool -> Type :=
    | mem_spec_1 : forall x s, In x s -> mem_spec_ind x s true
    | mem_spec_2 : forall x s, ~In x s -> mem_spec_ind x s false.
  Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
    intros.
    remember (add x (add y (singleton z))). (* remember is needed here *)
    destruct (mem_eq z t0). reflexivity. subst. apply False_ind. apply
n. setdec.
  Qed.

  Inductive add_spec : elt -> t -> t -> Type :=
  | add_spec_1 : forall x s s', (forall y, In y s' <-> (E.eq x y \/ In
y s)) -> add_spec x s s'.

  Lemma add_eq : forall x s, add_spec x s (add x s).
  Proof.
    intros.
    constructor.  intros. set_iff. reflexivity.
  Qed.

End Test.

thomas braibant

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Stéphane Lescuyer-3]

Hi Thomas,

> I was then told that I could use inductives, to do the same job.
> <--
> Inductive mem_spec_ind : elt -> t -> bool -> Type :=
>    | mem_spec_1 : forall x s, In x s -> mem_spec_ind x s true
>    | mem_spec_2 : forall x s, ~In x s -> mem_spec_ind x s false.
> Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.
> -->
>
> Unfortunately, "destruct"-ing mem_eq in a Goal can lead to the
> forgetting of useful informations. I have to remember some pieces of
> information by hand, while everything is smoother using the
> rewrite-destruct scheme.

You should just be careful writing the inductive spec : uniform
parameters are not the same thing as variables introduced in the
constructors. In that case, you should have written :

Inductive mem_spec_ind x s : bool -> Type :=
| mem_spec_1 : In x s -> mem_spec_ind x s true
| mem_spec_2 : ~In x s -> mem_spec_ind x s false.
Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.

and then destructing (mem_eq t1 t2) does not 'erase' t1 and t2, and
everything goes fine :

 Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1 else 2)= 1.
   intros.
   destruct (mem_eq z (add x (add y (singleton z)))).
   reflexivity.
   setdec.
 Qed.

Even with the 'wrong' definition you can also use inversion(_clear)
instead of destruct and you won't lose any information, but
unfortunately you'd have to explictely introduce the hypothesis to be
inverted. I'd like it a lot, actually, if the inversion tactic were to
work on arbitrary constructions instead of just hypotheses
identifiers.

On a more specific note, in your particular goal here, I'd rather use
existing lemmas and proceed without case split at all : rewrite twice
using EqProps.add_mem_3 and then EqProps.singleton_mem_1. If I can
give a direct proof, I tend to do it.

Cheers,

Stéphane
--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Guillaume Melquiond-3]

Stéphane Lescuyer a écrit :

> You should just be careful writing the inductive spec : uniform
> parameters are not the same thing as variables introduced in the
> constructors. In that case, you should have written :
>
> Inductive mem_spec_ind x s : bool -> Type :=
> | mem_spec_1 : In x s -> mem_spec_ind x s true
> | mem_spec_2 : ~In x s -> mem_spec_ind x s false.
> Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.
>
> and then destructing (mem_eq t1 t2) does not 'erase' t1 and t2, and
> everything goes fine :
>
>  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1 else 2)= 1.
>    intros.
>    destruct (mem_eq z (add x (add y (singleton z)))).

Stephane's solution is correct. I would just like to point that there is
a better tactic than "destruct" for this kind of inductives:

   case mem_eq. (* No arguments! Coq infers them when using "case". *)

Best regards,

Guillaume

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Matthieu Sozeau]

Le 19 oct. 09 à 09:44, Thomas Braibant a écrit :

<snip/>

> The goal here would be to be able to automatize such destructions, in
> order to be able to reason more easily on more complicated programs. I
> wonder if any function should have such a specification (like add,
> below).
> Inductive add_spec : elt -> t -> t -> Type :=
> | add_spec_1 : forall x s s', (forall y, In y s' <-> (E.eq x y \/ In y
> s)) -> add_spec x s s'.
> Lemma add_eq : forall x s, add_spec x s (add x s).

Hi Thomas,

You're basically building propositional views of your functions and want
to automate the transformation from bool to Prop. You can do that with
minimal verbosity using type classes, a few Ltac tricks and dependent
elimination (or, I suppose, using ssreflect's support for reflection
and dependent elimination). Here's my attempt:

<<

Require Import Equality Program FSets.
Require Import Sumbool.
Module Test (X : FSetInterface.S).
  Module OrdProps := FSetProperties.OrdProperties X.
  Module EqProps := FSetEqProperties.EqProperties X.
  Module Props := EqProps.MP.
  Module Facts  := Props.FM.
  Module Dec := Props.Dec.

  Include Facts.
  Include OrdProps.
  Import  X.
  Ltac setdec := Dec.fsetdec.

  Definition proj_sumbool {P Q} (x : {P} + {Q}) :=
    if x then true else false.

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
    intros.
    case_eq (mem z (add x (add y (singleton z)))); intro H.
      reflexivity.
      apply False_ind. revert H. rewrite <- not_mem_iff. set_iff.  
intuition.
  Qed.
  Lemma mem_dec : forall x s, {In x s} + {~ In x s}. Admitted.
  Lemma mem_proj : forall x s, mem x s = proj_sumbool (mem_dec x s).  
Admitted.

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
    intros.
    rewrite mem_proj. destruct mem_dec. reflexivity.
    apply False_ind. apply n. set_iff. intuition.
  Qed.

  Inductive mem_spec_ind : elt -> t -> bool -> Prop :=
    | mem_spec_1 : forall x s, In x s -> mem_spec_ind x s true
    | mem_spec_2 : forall x s, ~In x s -> mem_spec_ind x s false.
  Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.


  (* Apply dependent elimination to a term *)
  Ltac depelim_term t := let H := fresh in
    set (H := t) ; depelim H ;
      (* Rewrite with the last hyp that gives the equality between
         the result and the initial call *)
      try on_last_hyp ltac:(fun id => rewrite <- id ; clear id).

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
    else 2)= 1.
    intros. depelim_term (mem_eq z (add x (add y (singleton z)))).
    reflexivity. apply False_ind. apply H. setdec.
  Qed.

  (* Go further and add a class for propositional views of
     functions. This is kind of a dummy class as we can't
     express the form a view type should have here,
     but [prop_view_ty] should be [Π Δ, some_ind Δ (f Δ)]. *)

  Class PropView {A} (f : A) :=
    { prop_view_ty : Prop ; prop_view : prop_view_ty }.

  Instance mem_propview : PropView mem := { prop_view := mem_eq }.

  (* Now a tactic to destruct a call to a function using
     his associated propositional view. *)

  Ltac prop_view f :=
    (* Find the view associated with [f] *)
    let prf := constr:(prop_view (f:=f)) in
      on_call f ltac:(fun c =>
        match c with
          | appcontext args [ f ] =>
            let ind_app := context args [ prf ] in
            let H := fresh in
            let call := fresh in
              set(H := ind_app) ; (* The view proof *)
              set(call := c) in *; (* Abstract the call *)
              depelim H
        end).

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
    intros. prop_view mem.
    reflexivity. apply False_ind. apply H. setdec.
  Qed.

  Inductive add_spec : elt -> t -> t -> Type :=
  | add_spec_1 : forall x s s', (forall y, In y s' <-> (E.eq x y \/ In
y s)) -> add_spec x s s'.

  Lemma add_eq : forall x s, add_spec x s (add x s).
  Proof.
    intros.
    constructor.  intros. set_iff. reflexivity.
  Qed.

End Test.

 >>

Hope this helps,
-- Matthieu

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Stéphane Lescuyer-3]

On Mon, Oct 19, 2009 at 4:50 PM, Guillaume Melquiond
<guillaume.melquiond@...> wrote:
> Stephane's solution is correct. I would just like to point that there is a
> better tactic than "destruct" for this kind of inductives:
>
>  case mem_eq. (* No arguments! Coq infers them when using "case". *)
>

Good to know, indeed ! Any particular reason why destruct does not do
something similar ? Or does not accept holes, which would be
sufficient for that matter : destruct (mem_eq _ _) ?

Stéphane

--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Cody Roux]

On Tue, 2009-10-20 at 12:24 -0400, Vladimir Voevodsky wrote:
> Given an inductive type such as
>
> Inductive two_el := el_1 | el_2 .
>
> are there closed terms of type two_el which do not reduce to either  
> el_1 or el_2 ?

No. This can be deduced from the strong normalisation property of the
underlying calculus of Coq (CIC+Predicative Set+Universes), combined
with the Inversion Property: It is easy to show by case analysis that
any term in normal form and in the empty context of type two_el must be
one of the constructors of this type. This can be compared with the
disjunction property which states:

If t is a term of type A\/B in the empty context then t reduces to
inl t1   or to    inr t2

Which happens to be quite a desirable property in constructive
mathematics.

Cheers

Cody

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Cody Roux]

On Tue, 2009-10-20 at 12:43 -0400, Vladimir Voevodsky wrote:
> (cont.) Is it also true  that any closed term of type nat reduces to a  
> term of the form S ... S O ?
>
> V.
>
>
Also true, if as Adam has said, you work in a system without (non
computational) axioms. This can be generalized to all inductive types,
though one must notice that in the presence of dependent types, some
instances of the inductive types may be empty e.g.

Inductive ZeroEmpty: nat->Type:=
|Notzero: forall n, ZeroEmpty (S n)
.

In this case (ZeroEmpty 0) is uninhabited. Nevertheless, every term of
type (ZeroEmpty 0) in the empty context (in this case there are no such
terms) does reduce to (Notzero t).

Cody

>
> On Oct 20, 2009, at 6:38 AM, Cody Roux wrote:
>
> > On Tue, 2009-10-20 at 12:24 -0400, Vladimir Voevodsky wrote:
> >> Given an inductive type such as
> >>
> >> Inductive two_el := el_1 | el_2 .
> >>
> >> are there closed terms of type two_el which do not reduce to either
> >> el_1 or el_2 ?
> >
> > No. This can be deduced from the strong normalisation property of the
> > underlying calculus of Coq (CIC+Predicative Set+Universes), combined
> > with the Inversion Property: It is easy to show by case analysis that
> > any term in normal form and in the empty context of type two_el must  
> > be
> > one of the constructors of this type. This can be compared with the
> > disjunction property which states:
> >
> > If t is a term of type A\/B in the empty context then t reduces to
> > inl t1   or to    inr t2
> >
> > Which happens to be quite a desirable property in constructive
> > mathematics.
> >
> > Cheers
> >
> > Cody
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Cody Roux]

On Tue, 2009-10-20 at 13:04 -0400, Vladimir Voevodsky wrote:
> (cont.) Does it imply that in the empty context it is impossible to  
> define a function (nat -> nat) -> nat which maps f to its minimal value?
>
> V.
>
  Indeed. If you could define such a function, than you could take any
\Pi^0_1 sentence P (a proposition of one parameter n that is decidable
for each instance of that parameter), and define a function f:nat->nat
in Coq such that:

f n reduces to (S 0) if the proposition P(n) is true
f n reduces to    0  if the proposition P(n) is false

taking your min:(nat->nat)->nat function, we could decide of the truth
of such a sentence: it suffices to test whether (min f) reduces to 0 or
to 1 which it necessarily does by the previous argument. This would
allow us to solve the halting problem.

Hope this helps,

Cody

>
> On Oct 20, 2009, at 6:56 AM, Cody Roux wrote:
>
> > On Tue, 2009-10-20 at 12:43 -0400, Vladimir Voevodsky wrote:
> >> (cont.) Is it also true  that any closed term of type nat reduces  
> >> to a
> >> term of the form S ... S O ?
> >>
> >> V.
> >>
> >>
> > Also true, if as Adam has said, you work in a system without (non
> > computational) axioms. This can be generalized to all inductive types,
> > though one must notice that in the presence of dependent types, some
> > instances of the inductive types may be empty e.g.
> >
> > Inductive ZeroEmpty: nat->Type:=
> > |Notzero: forall n, ZeroEmpty (S n)
> > .
> >
> > In this case (ZeroEmpty 0) is uninhabited. Nevertheless, every term of
> > type (ZeroEmpty 0) in the empty context (in this case there are no  
> > such
> > terms) does reduce to (Notzero t).
> >
> > Cody
> >
> >
> >>
> >> On Oct 20, 2009, at 6:38 AM, Cody Roux wrote:
> >>
> >>> On Tue, 2009-10-20 at 12:24 -0400, Vladimir Voevodsky wrote:
> >>>> Given an inductive type such as
> >>>>
> >>>> Inductive two_el := el_1 | el_2 .
> >>>>
> >>>> are there closed terms of type two_el which do not reduce to either
> >>>> el_1 or el_2 ?
> >>>
> >>> No. This can be deduced from the strong normalisation property of  
> >>> the
> >>> underlying calculus of Coq (CIC+Predicative Set+Universes), combined
> >>> with the Inversion Property: It is easy to show by case analysis  
> >>> that
> >>> any term in normal form and in the empty context of type two_el must
> >>> be
> >>> one of the constructors of this type. This can be compared with the
> >>> disjunction property which states:
> >>>
> >>> If t is a term of type A\/B in the empty context then t reduces to
> >>> inl t1   or to    inr t2
> >>>
> >>> Which happens to be quite a desirable property in constructive
> >>> mathematics.
> >>>
> >>> Cheers
> >>>
> >>> Cody
> >>
>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Vladimir Voevodsky]

Given an inductive type such as

Inductive two_el := el_1 | el_2 .

are there closed terms of type two_el which do not reduce to either  
el_1 or el_2 ?

Vladimir.
 

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Adam Chlipala-3]

Vladimir Voevodsky wrote:
> Given an inductive type such as
>
> Inductive two_el := el_1 | el_2 .
>
> are there closed terms of type two_el which do not reduce to either
> el_1 or el_2 ?

That depends on the axioms that you assert.  With no axioms, I believe
the CIC consistency theorem guarantees the property you describe (modulo
differences between the real Coq implementation and the theory).

The axiom from the [Eqdep] module is a good example of a term that can
block complete reduction, but is very useful.  There is also the less
interesting case of trying to reduce terms that contain subterms marked
as opaque with [Qed] or similar.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Vladimir Voevodsky]

(cont.) Is it also true  that any closed term of type nat reduces to a  
term of the form S ... S O ?

V.



On Oct 20, 2009, at 6:38 AM, Cody Roux wrote:

> On Tue, 2009-10-20 at 12:24 -0400, Vladimir Voevodsky wrote:
>> Given an inductive type such as
>>
>> Inductive two_el := el_1 | el_2 .
>>
>> are there closed terms of type two_el which do not reduce to either
>> el_1 or el_2 ?
>
> No. This can be deduced from the strong normalisation property of the
> underlying calculus of Coq (CIC+Predicative Set+Universes), combined
> with the Inversion Property: It is easy to show by case analysis that
> any term in normal form and in the empty context of type two_el must  
> be
> one of the constructors of this type. This can be compared with the
> disjunction property which states:
>
> If t is a term of type A\/B in the empty context then t reduces to
> inl t1   or to    inr t2
>
> Which happens to be quite a desirable property in constructive
> mathematics.
>
> Cheers
>
> Cody

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[Vladimir Voevodsky]

(cont.) Does it imply that in the empty context it is impossible to  
define a function (nat -> nat) -> nat which maps f to its minimal value?

V.


On Oct 20, 2009, at 6:56 AM, Cody Roux wrote:

> On Tue, 2009-10-20 at 12:43 -0400, Vladimir Voevodsky wrote:
>> (cont.) Is it also true  that any closed term of type nat reduces  
>> to a
>> term of the form S ... S O ?
>>
>> V.
>>
>>
> Also true, if as Adam has said, you work in a system without (non
> computational) axioms. This can be generalized to all inductive types,
> though one must notice that in the presence of dependent types, some
> instances of the inductive types may be empty e.g.
>
> Inductive ZeroEmpty: nat->Type:=
> |Notzero: forall n, ZeroEmpty (S n)
> .
>
> In this case (ZeroEmpty 0) is uninhabited. Nevertheless, every term of
> type (ZeroEmpty 0) in the empty context (in this case there are no  
> such
> terms) does reduce to (Notzero t).
>
> Cody
>
>
>>
>> On Oct 20, 2009, at 6:38 AM, Cody Roux wrote:
>>
>>> On Tue, 2009-10-20 at 12:24 -0400, Vladimir Voevodsky wrote:
>>>> Given an inductive type such as
>>>>
>>>> Inductive two_el := el_1 | el_2 .
>>>>
>>>> are there closed terms of type two_el which do not reduce to either
>>>> el_1 or el_2 ?
>>>
>>> No. This can be deduced from the strong normalisation property of  
>>> the
>>> underlying calculus of Coq (CIC+Predicative Set+Universes), combined
>>> with the Inversion Property: It is easy to show by case analysis  
>>> that
>>> any term in normal form and in the empty context of type two_el must
>>> be
>>> one of the constructors of this type. This can be compared with the
>>> disjunction property which states:
>>>
>>> If t is a term of type A\/B in the empty context then t reduces to
>>> inl t1   or to    inr t2
>>>
>>> Which happens to be quite a desirable property in constructive
>>> mathematics.
>>>
>>> Cheers
>>>
>>> Cody
>>

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

[muad]

> Is it also true that any closed term of type nat reduces to a term of the form S ... S O

This is the definition of canonicity which I believe Coq has, although I am never sure about anything when coinductives are involved (Of course axioms and opaque terms can stop reduction).


> Does it imply that in the empty context it is impossible to define a function (nat -> nat) -> nat which maps f to its minimal value?

The existence of such a function would let you produce a mu-minimization operator and that contradicts the strong normalization of Coq, so lets say that it's not possible. I think that if you defined the term and its property as an axiom: You still have a consistent theory though.