LF tp : type =
| nat : tp
| arr : tp -> tp -> tp
;
--name tp A.
% Structural equality.
LF eq : tp → tp → type =
| eq_nat : eq nat nat
| eq_arr : eq A A' → eq B B' → eq (arr A B) (arr A' B')
;
% Reflexivity is admissible.
rec refl : {T : [ ⊢ tp] } [ ⊢ eq T T ] =
/ total t (refl t) /
mlam T ⇒ (case [ |- T] of
| [ |- nat] => [ ⊢ eq_nat ]
| [ |- arr T1 T2] =>
let [ ⊢ D1 ] = refl [ ⊢ T1 ] in
let [ ⊢ D2 ] = refl [ ⊢ T2 ] in
[ ⊢ eq_arr D1 D2 ]
)
;
LF tm : type =
| lam : tp -> (tm -> tm) -> tm
| app : tm -> tm -> tm
| zero : tm
| succ : tm -> tm
| natrec : tm -> (tm -> tm) -> tm -> tm
;
--name tm M.
LF oft : tm -> tp -> type =
| t_app : oft M (arr A B) -> oft N A -> oft (app M N) B
| t_abs : ({x : tm} oft x A -> oft (M x) B) -> oft (lam A M) (arr A B)
| t_zero : oft zero nat
| t_succ : oft M nat -> oft (succ M) nat
| t_natrec : oft M1 A -> ({x : tm} oft x A -> oft (M2 x) A) -> oft N nat -> oft (natrec M1 M2 N) A
;
schema ctx = some [t : tp] block x : tm, u : oft x t;
rec unique : {g : ctx} {M : [ g ⊢ tm ]} [ g ⊢ oft M A[] ] → [ g ⊢ oft M B[] ] → [ ⊢ eq A B ] =
/ total e (unique _ _ _ e) /
mlam g ⇒ mlam M => fn d1 => fn d2 =>
(case [g |- M] of
| [g |- zero] =>
let [ g ⊢ t_zero ] = d1 in
let [ g ⊢ t_zero ] = d2 in
% After matching, we see that the type of M in both
% cases must be nat, which we solve by reflexivity.
refl [ ⊢ _ ]
| [g |- succ M3] =>
let [ g ⊢ t_succ D1 ] = d1 in
let [ g ⊢ t_succ D2 ] = d2 in
% After matching, we see that the type of M in both
% cases must be nat, which we solve by reflexivity.
refl [ ⊢ _ ]
| [g |- #p1.1] =>
% d1 : [ g ⊢ oft #p1.1 A ]
% So how do we actually get out the typing derivation?
% In the context, each variable is associated with its typing derivation.
% recall that each block is of the form
% some [ t : tp ] block x : tm, u : oft x t
% so each variable *comes with* its typing derivation, in slot 2 of the block.
let [ g ⊢ #q1.2 ] = d1 in
let [ g ⊢ #r1.2 ] = d2 in
% after matching, we can solve with reflexivity, because
% Beluga ensures that variables in a context appear only
% once.
refl [ ⊢ _ ]
| [g |- lam A[] (\x. N)] =>
let [g ⊢ t_abs (\x. \u. E1)] = d1 in
let [g ⊢ t_abs (\x. \u. E2)] = d2 in
let [ ⊢ C ] =
% first we specify the new context in which the recursive call takes place
% we add a new block containing a term and a typing derivation for that term
unique [g, b : block x : tm, u : oft x A[] ]
% N lives in an extended context, and depends on its argument,
% so when we want to *use* N as the term for induction, we need
% to apply the identity substitution extended
% with b.1 which is the term.
[g, b ⊢ N[.., b.1] ]
% Then the two different typing derivations,
% which we can form from d1 and d2
% The typing derivations E1 and E2 live in extended contexts since they
% depend on the *term* as well as on the *typing derivation* for that term.
[ g, b ⊢ E1[.., b.1, b.2] ]
[ g, b ⊢ E2[.., b.1, b.2] ] in
% goal here: [ ⊢ eq (arr A y) (arr A x)
% and C : [ ⊢ eq y x ] (ih)
% prove A = A by refl, and then form eq_arr
let [ ⊢ R ] = refl [ ⊢ A ] in
[ ⊢ eq_arr R C ]
| [g |- app M4 M5] =>
let [g ⊢ t_app E1 E2] = d1 in
let [g ⊢ t_app E1' E2'] = d2 in
let [ ⊢ C ] =
unique [g] [g ⊢ M4] [ g ⊢ E1 ] [ g ⊢ E1' ] in
let [ ⊢ eq_arr EQ1 EQ2 ] = [ ⊢ C ] in
[ ⊢ EQ2 ]
| [g |- natrec M (\x. M1) M2] =>
% Inversion on d1 and d2.
let [g ⊢ t_natrec E1 (\x. \u. T1) B1] = d1 in
let [g ⊢ t_natrec E2 (\x. \u. T2) B2] = d2 in
%
% Recall natrec Z S N performs recursion on N with base case Z and step case S.
% The typing constructor t_natrec EZ ES EN packages proofs that:
% 1. EZ: The base case has type A
% 2. ES: The step case assumes a value of type A and produces an A.
% 3. EN: That N is in fact a natural number.
% The constructor states that the result type of the recursion is A.
%
% So E1 states that the base case has type A1 and E2
% states that the base case has type A2.
% Since these typing derivations are smaller, we can use
% the induction hypothesis to conclude that A1 = A2.
%
unique [g] [ g ⊢ _ ] [ g ⊢ E1 ] [ g ⊢ E2 ]
)
;