Library Can





Require
 Export
 Termes.

Hint
 Unfold
 iff: core
.







  Definition
 neutral t
 := forall
 u
 v
, t
 <> Abs u
 v
.




  Record
 is_cand (X
 : term -> Prop
) : Prop
 := 

    {incl_sn : forall
 t
, X
 t
 -> sn t
;

     clos_red : forall
 t
 u
, X
 t
 -> red t
 u
 -> X
 u
;

     clos_exp : forall
 t
, neutral t
 -> (forall
 u
, red1 t
 u
 -> X
 u
) -> X
 t
}.




  Lemma
 cand_sn : is_cand sn.

constructor
; intros
; auto
 with
 coc
.




apply
 sn_red_sn with
 t
; auto
 with
 coc
.




red
 in
 |- *; apply
 Acc_intro; auto
 with
 coc
.

Qed
.




  Hint
 Resolve
 cand_sn: coc
.




  Lemma
 var_in_cand : forall
 n
 X
, is_cand X
 -> X
 (Ref n
).

intros
.

apply
 (clos_exp X
); auto
 with
 coc
.

unfold
 neutral
 in
 |- *; intros
; discriminate
.




intros
.

inversion
 H0
.

Qed
.




  Lemma
 cand_sat :

   forall
 X
, is_cand X
 ->

   forall
 u
, sn u
 ->

   forall
 m
, X
 (subst u
 m
) ->

   forall
 T
, sn T
 ->

  X
 (App (Abs T
 m
) u
).

Proof
.

simple
 induction
 2.

clear
 u
 H0
; intros
 u
 _
 IHu
; unfold
 transp
 in
 *.

intros
 m
 m_in_X
.

generalize
 m_in_X
.

cut
 (sn m
).

2: apply
 sn_subst with
 u
; apply
 (incl_sn _
 H
); trivial
.

simple
 induction
 1.

clear
 m
 m_in_X
 H0
; intros
 m
 _
 IHm
 m_in_X
; unfold
 transp
 in
 *.

simple
 induction
 1.

clear
 T
 H0
; intros
 T
 acc_T
 IHT
; assert
 (sn_T
 := Acc_intro _
 acc_T
 : sn T
);

 clear
 acc_T
; unfold
 transp
 in
 *.

apply
 (clos_exp _
 H
). red
; intros
; discriminate
.

intros
 x
 red_redex
.

inversion_clear
 red_redex
; [idtac
|inversion_clear H0
|idtac].

trivial
.

auto
.

apply
 IHm
; trivial
.

apply
 clos_red with
 (subst u
 m
); trivial
.

unfold
 subst
; auto
 with
 coc
.

apply
 IHu
; auto
 with
 coc
.

apply
 clos_red with
 (subst u
 m
); trivial
.

unfold
 subst
; auto
 with
 coc
.

Qed
.







  Inductive
 skel : Set
 :=

    | PROP : skel

    | PROD : skel -> skel -> skel.




  Lemma
 EQ_skel : forall
 a
 b
 : skel, {a
=b}+{~a=b}.

Proof
.

decide
 equality
.

Qed
.




  Fixpoint
 Can (K
 : skel) : Type
 :=

    match
 K
 with


    | PROP => term -> Prop


    | PROD s1
 s2
 => Can s1
 -> Can s2


    end
.







  Definition
 eq_cand X
 Y
 := forall
 t
 : term, X
 t
 <-> Y
 t
.




  Hint
 Unfold
 eq_cand: coc
.




  Fixpoint
 eq_can (s
 : skel) : Can s
 -> Can s
 -> Prop
 :=

    match
 s
 return
 (Can s
 -> Can s
 -> Prop
) with


    | PROP => eq_cand

    | PROD s1
 s2
 =>

        fun
 C1
 C2
 => forall
 X1
 X2
, eq_can _
 X1
 X2
 -> eq_can _
 (C1
 X1
) (C2
 X2
)

    end
.




  Lemma
 eq_can_sym : forall
 s
 (X
 Y
 : Can s
), eq_can _
 X
 Y
 -> eq_can _
 Y
 X
.

Proof
.

simple
 induction
 s
; simpl
; intros
; auto
 with
 coc
.

unfold
 eq_cand
; intros
.

elim
 H
 with
 t
; auto
 with
 coc
.

Qed
.




Lemma
 eq_can_trans : forall
 s
 C1
 C2
 C3
,

   eq_can s
 C1
 C2
 -> eq_can s
 C2
 C3
 -> eq_can s
 C1
 C3
.

Proof
.

induction
 s
; simpl
; intros
.

red
; intros
.

case
 (H
 t
); case
 (H0
 t
); auto
.




prolog
 [eq_can_sym] 5.

Qed
.




Lemma
 eq_can_left: forall
 s
 C1
 C2
, eq_can s
 C1
 C2
 -> eq_can s
 C1
 C1
.

Proof
.

prolog
 [eq_can_trans eq_can_sym] 10.

Qed
.




Lemma
 eq_can_right: forall
 s
 C1
 C2
, eq_can s
 C1
 C2
 -> eq_can s
 C2
 C2
.

Proof
.

prolog
 [eq_can_trans eq_can_sym] 10.

Qed
.




  Lemma
 eq_cand_incl : forall
 t
 (X
 Y
 : Can PROP), eq_can _
 X
 Y
 -> X
 t
 -> Y
 t
.

Proof
.

intros
.

elim
 H
 with
 t
; auto
 with
 coc
.

Qed
.




  Lemma
 eq_can_prod : forall
 s1
 s2
 C1
 C2
,

    (forall
 X1
 X2
, eq_can _
 X1
 X2
 -> eq_can _
 (C1
 X1
) (C2
 X2
)) ->

    eq_can (PROD s1
 s2
) C1
 C2
.

Proof
.

simpl
; auto
.

Qed
.




  Lemma
 eq_can_prod_elim : forall
 s1
 s2
 C1
 C2
 X1
 X2
,

    eq_can (PROD s1
 s2
) C1
 C2
 ->

    eq_can _
 X1
 X2
 ->

    eq_can _
 (C1
 X1
) (C2
 X2
).

Proof
.

simpl
; intros
; prolog
 [eq_can_left eq_can_right] 5.

Qed
.




  Hint
 Resolve
 eq_can_prod eq_can_prod_elim : coc
.







  Fixpoint
 is_can (s
 : skel) : Can s
 -> Prop
 :=

    match
 s
 return
 (Can s
 -> Prop
) with


    | PROP => fun
 X
 => is_cand X


    | PROD s1
 s2
 =>

        fun
 C
 => eq_can _
 C
 C
 /\ (forall
 X
, is_can _
 X
 -> is_can _
 (C
 X
))

    end
.




  Lemma
 is_can_prop : forall
 X
, is_can PROP X
 -> is_cand X
.

Proof
.

trivial
.

Qed
.




  Hint
 Resolve
 is_can_prop: coc
.




  Lemma
 is_can_invariant : forall
 s
 C
, is_can s
 C
 -> eq_can s
 C
 C
.

Proof
.

induction
 s
; simpl
; red
; intros
; auto
; fold
 eq_can.

elim
 H
; intros
; auto
.

Qed
.




  Hint
 Resolve
 is_can_invariant: coc
.




  Lemma
 is_can_prod_elim : forall
 s1
 s2
 (F
:Can(PROD s1
 s2
)) X
,

    is_can _
 F
 ->

    is_can _
 X
 ->

    is_can _
 (F
 X
).

Proof
.

destruct
 1; fold
 is_can in
 *; auto
.

Qed
.







  Fixpoint
 default_can (s
 : skel) : Can s
 :=

    match
 s
 return
 (Can s
) with


    | PROP => sn

    | PROD s1
 s2
 => fun
 _
 => default_can s2


    end
.




  Lemma
 def_can_is_can : forall
 s
, is_can _
 (default_can s
).

Proof
.

simple
 induction
 s
; simpl
 in
 |- *; intros
; auto
 with
 coc
.

Qed
.




  Hint
 Resolve
 def_can_is_can : coc
.







  Definition
 Pi s
 (X
 : Can PROP) (F
 : Can (PROD s
 PROP)) : Can PROP :=

    fun
 t
 => forall
 u
 C
, X
 u
 -> is_can _
 C
 -> F
 C
 (App t
 u
).




  Lemma
 eq_can_Pi :

   forall
 s
 X
 Y
 F1
 F2
,

   eq_can _
 X
 Y
 -> eq_can _
 F1
 F2
 -> eq_can _
 (Pi s
 X
 F1
) (Pi s
 Y
 F2
).

simpl
 in
 |- *; intros
; unfold
 iff
, Pi
 in
 |- *.

split
; intros
.

elim
 H0
 with
 C
 C
 (App t
 u
); elim
 H
 with
 u
; auto
 with
 coc
.




elim
 H0
 with
 C
 C
 (App t
 u
); elim
 H
 with
 u
; auto
 with
 coc
.

Qed
.




  Lemma
 is_can_Pi :

   forall
 s
 X
 F
, is_cand X
 -> (forall
 C
, is_can _
 C
 -> is_cand (F
 C
)) -> is_cand (Pi s
 X
 F
).

simpl
 in
 |- *; unfold
 Pi
 in
 |- *;

 intros
 s
 X
 F
 X_can
 F_map_can
.

constructor
.

intros
 t
 app_in_can
.

apply
 subterm_sn with
 (App t
 (Ref 0)); auto
 with
 coc
.

apply
 (incl_sn (F
 (default_can s
))); auto
 with
 coc
.

apply
 app_in_can
; auto
 with
 coc
.

apply
 var_in_cand with
 (X
:=X); auto
 with
 coc
.




intros
.

apply
 (clos_red (F
 C
)) with
 (App t
 u0
); auto
 with
 coc
.




intros
 t
 t_neutr
 clos_exp_t
 u
 C
 u_in_C
 C_can
.

apply
 (clos_exp (F
 C
)); auto
 with
 coc
.

red
 in
 |- *; intros
; discriminate
.




generalize
 u_in_C
.

assert
 (u_sn
: sn u
).

apply
 (incl_sn X
); auto
 with
 coc
.

clear
 u_in_C
.

elim
 u_sn
.

intros
 v
 _
 v_Hrec
 v_in_X
 w
 red_w
.

generalize
 t_neutr
; clear
 t_neutr
.

inversion_clear
 red_w
; intros
; auto
 with
 coc
.

elim
 t_neutr
 with
 T
 M
; auto
 with
 coc
.




apply
 (clos_exp (F
 C
)); intros
; auto
 with
 coc
.

red
 in
 |- *; intros
; discriminate
.




apply
 v_Hrec
 with
 N2
; auto
 with
 coc
.

apply
 (clos_red X
) with
 v
; auto
 with
 coc
.

Qed
.




  Lemma
 Abs_sound :

   forall
 s
 A
 F
 T
 m
,

   is_can PROP A
 ->

   is_can (PROD s
 PROP) F
 ->

   (forall
 n
 (C
 : Can s
), A
 n
 -> is_can _
 C
 -> F
 C
 (subst n
 m
)) ->

   sn T
 -> Pi s
 A
 F
 (Abs T
 m
).

unfold
 Pi
 in
 |- *; intros
.

assert
 (is_cand (F
 C
)).

apply
 is_can_prop; apply
 is_can_prod_elim with
 (s1
:=s);

 auto
 10 with
 coc
.




apply
 (clos_exp (F
 C
)); intros
; auto
 with
 coc
.

red
 in
 |- *; intros
; discriminate
.




apply
 clos_red with
 (App (Abs T
 m
) u
); auto
 with
 coc
.

apply
 (cand_sat (F
 C
)); auto
 with
 coc
.

apply
 (incl_sn A
); auto
 with
 coc
.

Qed
.