The Coq mailing list

[Pierre CASTERAN <Pierre.Casteran AT labri.u-bordeaux.fr>]

 Hello,


 Just a question: 
 You may find below a little theory of sequences (finite or infinite).

 I had no problem to prove (in a classical framework) the disjunction :
 (s:(sequence A))(finite A s) \/ (infinite A s).

 But I failed to do that in the intuitionnistic framework.
 May i infer from my personal failure that the frontier between
 intuitionnist and classical deduction passes by this point ?

 Best regards,

Pierre

---------------------------------------------------------------------------
(* adapted from the "Stream" package *)


Section Sequences.

 Variable A :Set.

 CoInductive Set sequence := Empty : sequence
                           | Seq : A->sequence->sequence.


 Definition rest  := 
   [s:sequence]Cases s of Empty => Empty
                      | (Seq a s') => s'
               end.

 Definition head : sequence -> (Exc A) := 
  [x:sequence]Cases x of Empty => (error A)
                      | (Seq a s) => (value A a)
               end.
End Sequences.

Syntactic Definition seq := (Seq ?).
Syntactic Definition hd   := (head ?).
Syntactic Definition rst   := (rest ?).
Syntactic Definition empty := (Empty ?).

Section Basic_predicates.

 Variable A:Set.


 Inductive finite : (sequence A) -> Prop :=
   Empty_f : (finite empty)
 | Seq_f :  (a:A)(s:(sequence A))(finite s) ->
                            (finite (seq a s)).


 CoInductive infinite : (sequence A) -> Prop :=
  Seq_i : (a:A)(s:(sequence A))(infinite s) ->(infinite (seq a s)).


End Basic_predicates.

Section Basic_Lemmas.
Variable A:Set.


(* Finite/Infinite *)

(* Agradezco a Eduardo por los dos siguientes lemas *)

Lemma emptyNoInfinite : (s:(sequence A))(infinite ? s)->~s=empty.
Proof.
 Intros s H.
 Inversion H.
 Discriminate.
Qed.


Lemma restOfInfinite : (s:(sequence A))(infinite ? s)->(infinite ? (rst s)).
Proof.
 Intros s H.
 Inversion H.
 Assumption.
Qed.


Lemma finite_not_infinite:(s:(sequence A))(finite ? s)->~(infinite ? s).
Proof.
 Induction 1.
 Red;Intro H.
 Inversion H0;Discriminate.
 Intros.
 Red;Intro.
 Apply H1.
 Replace s0 with (rst (seq a s0)).
 Apply restOfInfinite;Auto.
 Simpl;Auto.
Qed.

Lemma not_finite_infinite:(s:(sequence A))~(finite ? s)->(infinite ? s).
Proof.
 Cofix.
 Destruct s.
 Intro;Absurd (finite A empty);Auto.
 Left.
 Intros.
 Split.
 Guarded.
 Apply not_finite_infinite.
 Guarded.
 Red;Intro;Apply H.
 Right;Auto. 
Qed.


Section Finite_or_infinite.
 Hypothesis tex :(P:Prop)P \/ ~P.


 Lemma finite_or_infinite: (s:(sequence A))(finite ? s) \/ (infinite ? s).
 Proof.
   Intro s;Case(tex (infinite ? s));[Auto|Intro].
   Left.
   Case (tex (finite ? s));[Auto|Intro].
   Absurd (infinite ? s).   
   Auto.
   Apply not_finite_infinite;Auto.
 Qed.

End Finite_or_infinite.

Lemma intuitionnistic_version:
 (s:(sequence A))(finite ? s) \/ (infinite ? s).
Abort.

End Basic_Lemmas.