1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda/sn.ma".
17 let rec substc M l on l ≝ match l with
19 | cons A D ⇒ lift (substc M D)[0≝A] 0 1
22 notation "M [ l ]" non associative with precedence 90 for @{'Substc $M $l}.
24 interpretation "Substc" 'Substc M l = (substc M l).
26 theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n.
27 #n #l (elim l) -l // #A #D #IH normalize >IH -IH. normalize //
30 (* REDUCIBILITY CANDIDATES ****************************************************)
33 inductive neutral: T → Prop ≝
34 | neutral_sort: ∀n.neutral (Sort n)
35 | neutral_rel: ∀i.neutral (Rel i)
36 | neutral_app: ∀M,N.neutral (App M N)
39 (* the reducibility candidates (r.c.) *)
40 record RC : Type[0] ≝ {
42 cr1 : ∀t. mem t → SN t;
43 sat0: ∀l,n. all mem l → mem (Appl (Sort n) l);
44 sat1: ∀l,i. all mem l → mem (Appl (Rel i) l);
45 sat2: ∀F,A,B,l. mem B → mem A →
46 mem (Appl F[0:=A] l) → mem (Appl (Lambda B F) (A::l))
49 interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
51 (* the r.c. of all s.n. terms *)
52 definition snRC: RC ≝ mk_RC SN ….
55 (* the carrier of the r.c. of a (dependent) product type *)
56 definition dep_mem ≝ λRA,RB,M. ∀N. N ∈ RA → App M N ∈ RB.
58 (* the r.c. of a (dependent) product type *)
59 axiom depRC: RC → RC → RC.
61 * ≝ λRA,RB. mk_RC (dev_mem RA RB) ?.
64 (* a generalization of mem on lists *)
65 let rec memc H l on l : Prop ≝ match l with
67 | cons A D ⇒ match H with
68 [ nil ⇒ A ∈ snRC ∧ memc H D
69 | cons R K ⇒ A ∈ R ∧ memc K D
73 interpretation "componentwise membership (context of reducibility candidates)" 'mem l H = (memc H l).
75 (* the r.c. associated to a type *)
76 let rec trc H t on t : RC ≝ match t with
78 | Rel i ⇒ nth i … H snRC
79 | App _ _ ⇒ snRC (* FG ??? *)
81 | Prod A B ⇒ depRC (trc H A) (trc (trc H A :: H) B)
82 | D _ ⇒ snRC (* FG ??? *)
85 notation "hvbox(〚T〛 _ term 90 E)" non associative with precedence 50 for @{'InterpE $T $E}.
87 interpretation "interpretation of a type" 'InterpE t H = (trc H t).
89 (* the r.c. context associated to a context *)
90 let rec trcc H G on G : list RC ≝ match G with
92 | cons A D ⇒ 〚A〛_(trcc H D) :: trcc H D
95 interpretation "interpretation of a context" 'InterpE G H = (trcc H G).
97 theorem tj_trc: ∀G,A,B. G ⊢A:B → ∀H,l. l ∈ 〚G〛_(H) →
98 A[l] ∈ 〚B[l]〛_〚G〛_(H).
99 #G #A #B #tjAB (elim tjAB) -G A B tjAB
100 [ #i #j #_ #H #l #_ >substc_sort >substc_sort @(sn_sort (nil ?)) //
101 | #G #B #n #tjB #IH #H #l (elim l) -l (normalize)
103 | #C #D #IHl #mem (elim mem) -mem #mem #memc
105 theorem tj_sn: ∀G,A,B. G ⊢A:B → SN A.
106 #G #A #B #tjAB lapply (tj_trc … tjAB (nil ?) (nil ?)) -tjAB (normalize) /3/