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


(*  BENCH OF Discriminate AND Injection  *)
(*  ==================================  *)

Theorem d_S_O : (n:nat) ~(O=(S n)).

 Intros ; Discriminate.
Save.

Theorem S_inj : (n,m:nat)(((S n)=(S m)) -> (n=m)).
  Intros n m H ; Injection H;Trivial.
Save.

Theorem s_inj2 : (n,m:nat)(((S (S n))=(S (S (S m)))) -> (n=(S m))).

  Intros.
  Injection H;Trivial.
Save.


(* ----------- Type dependant  ------------ *)

Inductive  Q [A:Set] : bool-> Set :=
     a : (Q A true)  | b: (Q A true) | c: (Q A false).

Theorem d_a_b :  (A:Set) ~((a A) = (b A)).

Intros ; Discriminate.
Save.


(* ----------- LIST --------- *)

Inductive list  [A:Set] :  Set :=
  nil: (list A) | cons :  A -> (list A)-> (list A).


Theorem d_nil_cons : (A:Set)(a:A)(l:(list A))~((nil A)=(cons A a l)).

 Intros ; Discriminate.
Save.


(* --------- LISTN ------------- *)

Inductive  listn [A:Set] : nat-> Set :=
  niln: (listn A O) | consn : (n:nat) A -> (listn A n)-> (listn A (S n)).

Theorem cons_inj : (A:Set)(n:nat)(a,a':A)(l,l':(listn A n))
              ( ((consn A n a l)=(consn A n a' l'))  -> (a=a')).

  Intros.
  Injection H;Trivial.
Save.

Theorem cons_inj2 : (n:nat)(a,a':nat)(l,l':(listn nat  n))
              ( ((consn nat  n (S (S a))  l)=(consn nat  n (S (S (S a'))) l')) 
                                 -> (a=(S a'))).

 Intros.
 Injection H;Trivial.
Save.


(* ---------- LAMBDA ------------- *)

Inductive lambda : Set :=
    Ref : nat -> lambda
  | Abs : lambda -> lambda
  | App : lambda -> lambda -> lambda.


Theorem d_Ref_Abs : (l:lambda)(n:nat) ~((Ref n)=(Abs l)).

Intros ; Discriminate.
Save.


Theorem ref_inj : (a,b:nat) ( ((Ref a)=(Ref b)) -> (a = b) ).

  Intros.
  Injection H;Trivial.
Save.


Theorem app_inj1 : (a,a1,b,b1:lambda) ( ((App a  b)=(App a1 b1)) ->(a=a1) ).

 Intros.
 Injection H;Trivial.
Save.

Theorem app_inj2 : (a,a1,b,b1:lambda) ( ((App a  b)=(App a1 b1)) ->(b=b1) ).

 Intros.
 Injection H;Trivial.
Save.


(* -------  Z -------- *)
Inductive Z : Set := OZ: Z | pos: nat -> Z | neg: nat -> Z.

Theorem d_pos_neg : (n,m:nat)~((pos n)=(neg m)).

 Intros ; Discriminate.
Save.

Theorem pos_inj : (n, m: nat) ( ((pos n) = (pos m)) -> (n=m) ).

 Intros.
 Injection H;Trivial.
Save.


(* --------- ML_EXP --------- *)

Parameter OP:Set.

Parameter eval_op:OP->nat->nat->nat.

Definition  Pat:=nat.

Inductive MLexp : Set :=
  Bool:bool->MLexp
 |Num:nat->MLexp
 |op:OP->MLexp
 |id:Pat->MLexp
 |appl:MLexp->MLexp->MLexp
 |mlpair:MLexp->MLexp->MLexp
 |mllambda:Pat->MLexp->MLexp
 |let':Pat->MLexp->MLexp->MLexp
 |letrec:Pat->Pat->MLexp->MLexp->MLexp
 |ite:MLexp->MLexp->MLexp->MLexp.


Inductive V_E:bool->Set:=
  boolean:bool->(V_E true)
 |num:nat->(V_E true)
 |valpair:(V_E true)->(V_E true)->(V_E true)
 |OP_clos:OP->(V_E true)
 |Clos:Pat->MLexp->(V_E false)->(V_E true)
 |Clos_rec:Pat->MLexp->Pat->(V_E false)->(V_E true)
 |Enil:(V_E false)
 |Econs:Pat->(V_E true)->(V_E false)->(V_E false).

Theorem d_boolean_num : (b:bool)(n:nat) ~((boolean b)=(num n)).

 Intros ; Discriminate.
Save.


Theorem valpair_inj : (a,a1,b,b1: (V_E true)) ( ((valpair a b)=(valpair a1 b1)) -> (a=a1)).

 Intros.
 Injection H;Trivial.
Save.

Theorem boolean_inj : (a,a1:bool)( ((boolean a)=(boolean a1))-> (a=a1)).

 Intros.
 Injection H;Trivial.
Save.


(*------Lambda Sigma ... ------*)

Inductive TS: bool->Set
:=   var:nat->(TS false)
  | app:(TS false)->(TS false)->(TS false)
  | lam:(TS false)->(TS false)
  | env:(TS false)->(TS true)->(TS false)
  | ide:(TS true)
  | shift:(TS true)
  | scons:(TS false)->(TS true)->(TS true)
  | comp:(TS true)->(TS true)->(TS true)
  | lift:(TS true)->(TS true)
  | meta_X:nat->(TS false)
  | meta_x:nat->(TS true).

Definition terms := (TS false).

Definition substitutions := (TS true).

Theorem proj_app1  :  (n1,n2:nat) ( ((var n1)=(var n2))-> (n1=n2)).

  Intros.
  Injection H;Trivial.
Save.

Theorem  proj_app2 :  (a1,b1,a2,b2:terms) ( ((app a1 b1)=(app a2 b2)) -> (b1=b2)) .

 Intros.
 Injection H;Trivial.
Save.




(* -------- Process -------- *)

Inductive Set Process [A:Set]  := 
	LISTEN : (A->(Process A))->(Process A) |
	TALK   :  A->(Process A)->(A->(Process A))->(Process A) |
	PAR    : (Process A)->(Process A)->(Process A).


Theorem listen_inj1: (A:Set)(p,f:A->(Process A))(LISTEN A p)=(LISTEN A f)->p=f.
Intros. Injection H;Trivial.
Save.

Theorem listen_inj2: (A:Set)(p,f:A->(Process A))(LISTEN A p)=(LISTEN A f)->p=f.
Intros;Injection H;Trivial; Auto.
Save.


Theorem listen_talk_discr1: 
  (A:Set)(P:(Process A)) (p:A->(Process A))(v:A) ~(LISTEN A p)= (TALK A v P p).
Intros; Discriminate.
Save.

Theorem listen_talk_discr2: 
  (A:Set)(P:(Process A)) (p:A->(Process A))(v:A) ~(LISTEN A p)= (TALK A v P p).
Intros; Unfold not. 
Intro; Discriminate H.
Save.

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