(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                              DemoLinear.v                                *)
(****************************************************************************)

(*
  Direct Predicate Calculus is the fragment of First Order Predicate Calculus
  which is provable in Gentzen Sequent Calculus without the contraction
  rule. In [1], a decision procedure is given for Direct Predicate Calculus.
  
  As a master's thesis project, an intuitionistic version of this procedure has
  been implemented in the Coq system, as a tactic called "Linear"
  (Direct Predicate Calculus is strongly connected with the multiplicative
  fragment of Linear Logic. See [3]).
  The implementation is partially based on the method given in [2], but
  also deals with non-prenex formulas when possible.

  One can use "Linear" directly on the current goal, using the command
  "Linear." It introduces the external universal quantification, then applies
  the decision procedure. It leaves the goal unchanged when it fails.

  One can also use hypotheses and lemmas, with the command
  "Linear with c1 ... cn.", which has the same effect as applying "Linear"
  on the goal c1 -> ... -> cn -> g, where g is the current goal.

  [1] J. Ketonen and R. Weyhrauch. "A decidable fragment of Predicate
      Calculus". Theoretical Computer Science, 32:297-307, 1984.

  [2] G. Bellin and J. Ketonen. "A decision procedure revisited : Notes on
      direct logic, linear logic and its implementation". Theoretical
      Computer Science, 95:115-142, 1992.

  [3] J.-Y. Girard. "Linear Logic". Theoretical Computer Science,
      50:1-102, 1987.
                                                                         *)
(*************************************************************************)

Require Linear.

   (*** First Order examples ***)
   (****************************)


Section examples.

Variable a,b,c : nat.
Variable P,Q,odd,even : nat->Prop.
Variable f : nat -> nat.

Theorem E1 : (x:nat)(EX y:nat | ((P x)->(P y))).
Linear.
Save.

Theorem E2 : (EX x:nat |(P x))
             -> ((y:nat)(P y) -> (Q y))
             -> (EX z:nat |(Q z)).
Linear.
Save.

Theorem E3 : (even a) 
              -> ((x:nat)((even x)->(odd (S x))))
              -> (EX y:nat |(odd y)).
Linear.
Save.

Theorem E4 : ((x:nat)((and (P x) (odd x)) -> (even (f x))))
     -> ((x:nat)((even x)->(odd (S x))))
     -> (even a)
     -> (P (S a))
     -> (EX z:nat |(even (f z))).
Linear.
Save.

End examples.



  (*** The drinker's theorem ***)
  (*****************************)

Section drinkers.

Variable U : Set.
Variable Q : U -> Prop.

Axiom excluded_middle : (P:Prop) (P \/ ~P).

Lemma em_Q : (x:U) (Q x) \/ ~(Q x).
Exact [x:U](excluded_middle (Q x)).
Save.

Theorem  Drinker's_theorem : (x:U)(EX x:U |((Q x) -> (x: U) (Q x))).
Intro t0.
Generalize (excluded_middle (EX x:U |~(Q x))); Intro H; Elim H.
Linear.
Intro H0.
Exists t0.
Linear with H0 em_Q.
Save.

End drinkers.

   (*** Using axioms and hypothesis ***)
   (*** Linear with c1 ... cn.      ***)
   (***********************************)

Section Linear_with.

Variable le : nat -> nat -> Prop.
Variable f  : nat -> nat.
Variable P  : nat -> Prop.

Axiom le_n : (n:nat)(le n n).
Axiom le_S : (n,m:nat)(le n m) -> (le n (S m)).
Axiom monoticity : (n,m:nat)(le n m) -> (le (f n) (f m)).

Lemma le_x_Sx  : (x:nat)(le x (S x)).
Linear with le_n le_S.
Save.

Theorem L1 : (a:nat)(EX b:nat |(le (f a) b)).
Linear with le_n monoticity.
Save.

Theorem L2 : (a:nat)(EX b:nat |(le (f a) b)).
Linear with le_x_Sx monoticity.
Save.

End Linear_with.

   (*** Some non-linear examples                 ***)
   (*** The "Linear" tactic fails on these goals ***)
   (************************************************)
 
Section nonlinear.

Parameter A,B,C,D : Prop.

Theorem T1 : A -> (A /\ A).
Auto.
Save.

Theorem T2 : ((or A B) -> C) 
        -> (or (D -> A) (D -> B))
        -> D -> C.
Intros H H0 H1.
Elim H0; Auto.
Save.

End nonlinear.


(* $Id: DemoLinear.v,v 1.8 1999/06/29 07:48:38 loiseleu Exp $ *)
