LF ty : type =
| base : ty
| arr : ty → ty → ty
| sum : ty → ty → ty;
LF tm : ty → type =
| abs : (tm A → tm B) → tm (arr A B)
| app : tm (arr A B) → tm A → tm B
| inl : {B : ty} (tm A → tm (sum A B))
| inr : {A : ty} (tm B → tm (sum A B))
| match : tm (sum A B) → (tm A → tm C) → (tm B → tm C) → tm C;
schema cxt = tm A;
LF step : tm A → tm A → type =
| rbeta : step (app (abs M) N) (M N)
| rabs : ({x : tm A} (step (M x) (M' x))) → step (abs M) (abs M')
| rappl : step M M' → step (app M N) (app M' N)
| rappr : step N N' → step (app M N) (app M N')
| rinl : step M N → step (inl B M) (inl B N)
| rinr : step M N → step (inr A M) (inr A N)
| rcase : step M M' → step (match M N1 N2) (match M' N1 N2)
| rcinl : step (match (inl B M) N1 N2) (N1 M)
| rcinr : step (match (inr A M) N1 N2) (N2 M)
| rcl : ({x : tm A} (step (N x) (N' x))) → step (match M N N2) (match M N' N2)
| rcr : ({x : tm B} (step (N x) (N' x))) → step (match M N1 N) (match M N1 N');
LF mstep : tm A → tm A → type =
| m-refl : mstep M M
| m-step : step M N → mstep N M' → mstep M M';
rec m-trans : (g:cxt) {M1 : [g ⊢ tm A[]]} [g ⊢ mstep M1 M] → [g ⊢ mstep M M2] → [g ⊢ mstep M1 M2] / total s1 ( m-trans g a m1 m2 m s1 ) / =
mlam M1 ⇒ fn s1 ⇒ fn s2 ⇒ case s1 of
| [g ⊢ m-refl] ⇒ s2
| [g ⊢ m-step S MS] ⇒
let [g ⊢ MS'] = m-trans [g ⊢ _] [g ⊢ MS] s2 in [g ⊢ m-step S MS'];
rec mstep_appl : (g:cxt) {M : [g ⊢ tm (arr A[] B[])]} {M' : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} [g ⊢ mstep M M'] → [g ⊢ mstep (app M N) (app M' N)] / total ms ( mstep_appl g a b m m' n ms ) / =
mlam M ⇒ mlam M' ⇒ mlam N ⇒ fn ms ⇒ case ms of
| [g ⊢ m-refl] ⇒ [g ⊢ m-refl]
| [g ⊢ m-step S MS'] ⇒
let [_ ⊢ MS''] = mstep_appl [_ ⊢ _] [_ ⊢ M'] [_ ⊢ N] [_ ⊢ MS'] in [g ⊢ m-step (rappl S) MS''];
rec mstep_appr : (g:cxt) {M : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} {N' : [g ⊢ tm A[]]} [g ⊢ mstep N N'] → [g ⊢ mstep (app M N) (app M N')] / total ms ( mstep_appr g a b m n n' ms ) / =
mlam M ⇒ mlam N ⇒ mlam N' ⇒ fn ms ⇒ case ms of
| [g ⊢ m-refl] ⇒ [g ⊢ m-refl]
| [g ⊢ m-step S MS'] ⇒
let [_ ⊢ MS''] = mstep_appr [_ ⊢ M] [_ ⊢ _] [_ ⊢ N'] [_ ⊢ MS'] in [g ⊢ m-step (rappr S) MS''];
rec mstep_abs : (g:cxt) {M : [g, x : tm A[] ⊢ tm B[]]} [g, x : tm A[] ⊢ mstep M M'] → [g ⊢ mstep (abs (λx. M)) (abs (λx. M'))] / total ms ( mstep_abs g a b m m' ms ) / =
mlam M ⇒ fn s1 ⇒ case s1 of
| [g, x : tm A[] ⊢ m-refl] ⇒ [g ⊢ m-refl]
| [g, x : tm A[] ⊢ m-step S MS] ⇒
let [g ⊢ MS'] = mstep_abs [g, x : tm A[] ⊢ _] [g, x : tm A[] ⊢ MS] in
let [g ⊢ S'] = [g ⊢ rabs (λx. S)] in [g ⊢ m-step S' MS'];
rec mstep_inl : (g:cxt) {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} {B : [ ⊢ ty]} [g ⊢ mstep M M'] → [g ⊢ mstep (inl B[] M) (inl B[] M')] / total ms ( mstep_inl g a m m' b ms ) / =
mlam M ⇒ mlam M' ⇒ mlam B ⇒ fn ms ⇒ case ms of
| [g ⊢ m-refl] ⇒ [g ⊢ m-refl]
| [g ⊢ m-step S MS'] ⇒
let [_ ⊢ MS''] = mstep_inl [_ ⊢ _] [_ ⊢ _] [ ⊢ B] [_ ⊢ MS'] in [g ⊢ m-step (rinl S) MS''];
rec mstep_inr : (g:cxt) {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} {B : [ ⊢ ty]} [g ⊢ mstep M M'] → [g ⊢ mstep (inr B[] M) (inr B[] M')] / total ms ( mstep_inr g a m m' b ms ) / =
mlam M ⇒ mlam M' ⇒ mlam B ⇒ fn ms ⇒ case ms of
| [g ⊢ m-refl] ⇒ [g ⊢ m-refl]
| [g ⊢ m-step S MS] ⇒
let [_ ⊢ MS'] = mstep_inr [_ ⊢ _] [_ ⊢ _] [ ⊢ B] [_ ⊢ MS] in [g ⊢ m-step (rinr S) MS'];
rec mstep_match : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {M' : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} [g ⊢ mstep M M'] → [g ⊢ mstep (match M (λx. N1) (λy. N2)) (match M' (λx. N1) (λy. N2))] / total ms ( mstep_match g a b c m m' n1 n2 ms ) / =
mlam M ⇒ mlam M' ⇒ mlam N1 ⇒ mlam N2 ⇒ fn ms ⇒ case ms of
| [g ⊢ m-refl] ⇒ [g ⊢ m-refl]
| [g ⊢ m-step S MS] ⇒
let [_ ⊢ MS'] = mstep_match [_ ⊢ _] [_ ⊢ M'] [_ ⊢ N1] [_ ⊢ N2] [_ ⊢ MS] in [g ⊢ m-step (rcase S) MS'];
rec mstep_matchl : (g:cxt) {N : [g, x : tm A[] ⊢ tm C[]]} {N' : [g, x : tm A[] ⊢ tm C[]]} {M : [g ⊢ tm (sum A[] B[])]} {N2 : [g, y : tm B[] ⊢ tm C[]]} [g, x : tm A[] ⊢ mstep N N'] → [g ⊢ mstep (match M (λx. N) (λy. N2)) (match M (λx. N') (λy. N2))] / total ms ( mstep_matchl g a c b n n' m n2 ms ) / =
mlam N ⇒ mlam N' ⇒ mlam M ⇒ mlam N2 ⇒ fn ms ⇒ case ms of
| [g, x : tm A[] ⊢ m-refl] ⇒ [g ⊢ m-refl]
| [g, x : tm A[] ⊢ m-step S MS] ⇒
let [_ ⊢ MS'] = mstep_matchl [_ ⊢ _] [_ ⊢ N'] [_ ⊢ M] [_ ⊢ N2] [_ ⊢ MS] in [g ⊢ m-step (rcl (λx. S)) MS'];
rec mstep_matchr : (g:cxt) {N : [g, x : tm B[] ⊢ tm C[]]} {N' : [g, x : tm B[] ⊢ tm C[]]} {M : [g ⊢ tm (sum A[] B[])]} {N1 : [g, y : tm A[] ⊢ tm C[]]} [g, x : tm B[] ⊢ mstep N N'] → [g ⊢ mstep (match M (λx. N1) (λy. N)) (match M (λx. N1) (λy. N'))] / total ms ( mstep_matchr g b c a n n' m n1 ms ) / =
mlam N ⇒ mlam N' ⇒ mlam M ⇒ mlam N1 ⇒ fn ms ⇒ case ms of
| [g, x : tm B[] ⊢ m-refl] ⇒ [g ⊢ m-refl]
| [g, x : tm B[] ⊢ m-step S MS] ⇒
let [_ ⊢ MS'] = mstep_matchr [_ ⊢ _] [_ ⊢ N'] [_ ⊢ M] [_ ⊢ N1] [_ ⊢ MS] in [g ⊢ m-step (rcr (λx. S)) MS'];
rec subst_mred : (g:cxt) {M : [g, x : tm A[] ⊢ tm B[]]} {N : [g ⊢ tm A[]]} {N' : [g ⊢ tm A[]]} [g ⊢ step N N'] → [g ⊢ mstep M[…, N] M[…, N']] / trust / =
mlam M ⇒ mlam N ⇒ mlam N' ⇒ fn s ⇒ case [_, x : tm _ ⊢ M] of
| [g, x : tm A[] ⊢ x] ⇒ let [g ⊢ S] = s in [g ⊢ m-step S m-refl]
| [g, x : tm A[] ⊢ #p[…]] ⇒ [g ⊢ m-refl]
| [g, x : tm A[] ⊢ abs (λy. M)] ⇒
let [g ⊢ S] = s in let [g, y : tm _ ⊢ S'] =
subst_mred [g, y : tm _, x : tm A[] ⊢ M[…, x, y]] [g, y : tm _ ⊢ N[…]] [g, y : tm _ ⊢ N'[…]] [g, y : tm _ ⊢ S[…]] in
mstep_abs [g, y : tm _ ⊢ _] [g, y : tm _ ⊢ S']
| [g, x : tm A[] ⊢ app M1 M2] ⇒
let [g ⊢ S1] = subst_mred [g, x : tm A[] ⊢ M1] [g ⊢ N] [g ⊢ N'] s in
let [g ⊢ S2] = subst_mred [g, x : tm A[] ⊢ M2] [g ⊢ N] [g ⊢ N'] s in
let [g ⊢ MS1] =
mstep_appl [g ⊢ M1[…, N]] [g ⊢ M1[…, N']] [g ⊢ M2[…, N]] [g ⊢ S1] in
let [g ⊢ MS2] =
mstep_appr [g ⊢ M1[…, N']] [g ⊢ M2[…, N]] [g ⊢ M2[…, N']] [g ⊢ S2] in m-trans [g ⊢ _] [g ⊢ MS1] [g ⊢ MS2]
| [g, x : tm A[] ⊢ inl B[] M] ⇒
let [_ ⊢ MS] = subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] s in mstep_inl [g ⊢ M[…, N]] [g ⊢ M[…, N']] [ ⊢ B] [_ ⊢ MS]
| [g, x : tm A[] ⊢ inr B[] M] ⇒
let [_ ⊢ MS] = subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] s in mstep_inr [_ ⊢ _] [_ ⊢ _] [ ⊢ B] [_ ⊢ MS]
| [g, x : tm A[] ⊢ match M (λx. N1) (λy. N2)] ⇒
let [_ ⊢ S] = s in let [_ ⊢ S0] =
subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] s in
let [g, y : tm B[] ⊢ S1] =
subst_mred [g, y : tm _, x : tm A[] ⊢ N1[…, x, y]] [g, y : tm _ ⊢ N[…]] [g, y : tm _ ⊢ N'[…]] [g, y : tm _ ⊢ S[…]] in
let [g, y : tm C[] ⊢ S2] =
subst_mred [g, y : tm _, x : tm A[] ⊢ N2[…, x, y]] [g, y : tm _ ⊢ N[…]] [g, y : tm _ ⊢ N'[…]] [g, y : tm _ ⊢ S[…]] in
let [g, x : tm A[], y : tm B[] ⊢ N1'] = [_ ⊢ N1] in
let [g ⊢ MS0] =
mstep_match [g ⊢ M[…, N]] [g ⊢ M[…, N']] [g, y : tm B[] ⊢ N1[…, N[…], y]] [g, y : tm C[] ⊢ N2[…, N[…], y]] [_ ⊢ S0] in
let [g ⊢ MS1] =
mstep_matchl [g, y : tm B[] ⊢ N1[…, N[…], y]] [g, y : tm B[] ⊢ N1[…, N'[…], y]] [g ⊢ M[…, N']] [g, y : tm C[] ⊢ N2[…, N[…], y]] [_ ⊢ S1] in
let [g ⊢ MS2] =
mstep_matchr [g, y : tm C[] ⊢ N2[…, N[…], y]] [g, y : tm C[] ⊢ N2[…, N'[…], y]] [g ⊢ M[…, N']] [g, y : tm B[] ⊢ N1[…, N'[…], y]] [_ ⊢ S2] in
m-trans [_ ⊢ _] [_ ⊢ MS0] (m-trans [_ ⊢ _] [_ ⊢ MS1] [_ ⊢ MS2]);
inductive Sn : {g : cxt} → {M : [g ⊢ tm A[]]} → ctype =
| Acc : {g : cxt} {A : [ ⊢ ty]} {M : [g ⊢ tm A[]]} ({M' : [g ⊢ tm A[]]} {S : [g ⊢ step M M']} Sn [g ⊢ M']) → Sn [g ⊢ M];
rec mstep_sn : (g:cxt) {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} [g ⊢ mstep M M'] → Sn [g ⊢ M] → Sn [g ⊢ M'] / total sn ( mstep_sn g m m' ms sn ) / =
mlam M ⇒ mlam M' ⇒ fn ms ⇒ fn sn ⇒ case ms of
| [g ⊢ m-refl] ⇒ sn
| [g ⊢ m-step S MS'] ⇒
let Acc ([g]) ([ ⊢ A]) ([g ⊢ _]) r = sn in
let sn' = r [_ ⊢ _] [_ ⊢ S] in mstep_sn [_ ⊢ _] [_ ⊢ M'] [_ ⊢ MS'] sn';
inductive SN : {g : cxt} → {M : [g ⊢ tm A[]]} → ctype =
| SNeu : SNe [g ⊢ R] → SN [g ⊢ R]
| SAbs : SN [g, x : tm A[] ⊢ M] → SN [g ⊢ abs (λx. M)]
| SRed : SNRed [g ⊢ M] [g ⊢ M'] → SN [g ⊢ M'] → SN [g ⊢ M]
| SInl : SN [g ⊢ M] → SN [g ⊢ inl _ M]
| SInr : SN [g ⊢ M] → SN [g ⊢ inr _ M]
and inductive SNe : {g : cxt} → {M : [g ⊢ tm A[]]} → ctype =
| SVar : {#p : [g ⊢ tm A[]]} SNe [g ⊢ #p]
| SApp : SNe [g ⊢ R] → SN [g ⊢ M] → SNe [g ⊢ app R M]
| SCase : SNe [g ⊢ M] → SN [g, x : tm A[] ⊢ N1] → SN [g, y : tm B[] ⊢ N2] → SNe [g ⊢ match M (λx. N1) (λy. N2)]
and inductive SNRed : {g : cxt} → {M : [g ⊢ tm A[]]} → {M' : [g ⊢ tm A[]]} → ctype =
| SBeta : {M : [g, x : tm A[] ⊢ tm B[]]} SN [g ⊢ N] → SNRed [g ⊢ app (abs (λx. M)) N] [g ⊢ M[…, N]]
| SAppl : SNRed [g ⊢ R] [g ⊢ R'] → SNRed [g ⊢ app R M] [g ⊢ app R' M]
| SCInl : SN [g ⊢ M] → SN [g, x : tm A[] ⊢ N1] → SN [g, y : tm B[] ⊢ N2] → SNRed [g ⊢ match (inl B[] M) (λx. N1) (λy. N2)] [g ⊢ N1[…, M]]
| SCInr : SN [g ⊢ M] → SN [g, x : tm A[] ⊢ N1] → SN [g, y : tm B[] ⊢ N2] → SNRed [g ⊢ match (inr A[] M) (λx. N1) (λy. N2)] [g ⊢ N2[…, M]]
| SRCase : SNRed [g ⊢ M] [g ⊢ M'] → {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} SNRed [g ⊢ match M (λx. N1) (λy. N2)] [g ⊢ match M' (λx. N1) (λy. N2)];
inductive SnRed : {g : cxt} → {M : [g ⊢ tm A[]]} → {M' : [g ⊢ tm A[]]} → ctype =
| SnBeta : {M : [g, x : tm A[] ⊢ tm B[]]} Sn [g ⊢ N] → SnRed [g ⊢ app (abs (λx. M)) N] [g ⊢ M[…, N]]
| SnAppl : SnRed [g ⊢ M] [g ⊢ M'] → SnRed [g ⊢ app M N] [g ⊢ app M' N]
| SnCInl : Sn [g ⊢ M] → Sn [g, x : tm A[] ⊢ N1] → Sn [g, y : tm B[] ⊢ N2] → SnRed [g ⊢ match (inl B[] M) (λx. N1) (λy. N2)] [g ⊢ N1[…, M]]
| SnCInr : Sn [g ⊢ M] → Sn [g, x : tm A[] ⊢ N1] → Sn [g, y : tm B[] ⊢ N2] → SnRed [g ⊢ match (inr A[] M) (λx. N1) (λy. N2)] [g ⊢ N2[…, M]]
| SnCasR : SnRed [g ⊢ M] [g ⊢ M'] → {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} SnRed [g ⊢ match M (λx. N1) (λy. N2)] [g ⊢ match M' (λx. N1) (λy. N2)];
empty : type.
rec varSn : (g:cxt) {#p : [g ⊢ tm A[]]} Sn [g ⊢ #p] / total ( varSn ) / =
mlam p ⇒ let [_ ⊢ #p] : [g ⊢ tm A[]]= [_ ⊢ #p] in Acc [g] [ ⊢ A] [g ⊢ #p] (mlam M' ⇒ mlam S ⇒ impossible [_ ⊢ S]);
rec abs_sn : {g : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {M : [g, x : tm A[] ⊢ tm B[]]} Sn [g, x : tm A[] ⊢ M] → Sn [g ⊢ abs (λx. M)] / total s ( abs_sn g a b m s ) / =
mlam g ⇒ mlam A ⇒ mlam B ⇒ mlam M ⇒ fn sn ⇒ Acc [g] [ ⊢ arr A B] [g ⊢ abs (λx. M)] (mlam Q ⇒ mlam S ⇒
let [g ⊢ rabs (λx. S1)] = [g ⊢ S] in
let [g, x : tm A[] ⊢ S1] : [g, x : tm A[] ⊢ step M M1]=
[g, x : tm _ ⊢ S1] in let Acc ([g, x : tm A[]]) ([ ⊢ B]) ([g, x : tm A[] ⊢ M]) r =
sn in abs_sn [g] [ ⊢ A] [ ⊢ B] [g, x : tm A[] ⊢ M1] (r [g, x : tm A[] ⊢ M1] [g, x : tm A[] ⊢ S1]));
rec app_sna : (g:cxt) {M : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Sn [g ⊢ app M N] → Sn [g ⊢ M] / total s ( app_sna g a b m n s ) / =
mlam M ⇒ mlam N ⇒ fn sn ⇒
let Acc ([g]) ([ ⊢ B[]]) ([g ⊢ app M N]) r = sn in Acc [_] [_ ⊢ _] [_ ⊢ _] (mlam M' ⇒ mlam S ⇒ app_sna [_ ⊢ M'] [_ ⊢ _] (r [_ ⊢ app M' N] [_ ⊢ rappl S]));
rec app_snb : (g:cxt) {M : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Sn [g ⊢ app M N] → Sn [g ⊢ N] / total s ( app_snb g a b m n s ) / =
mlam M ⇒ mlam N ⇒ fn sn ⇒
let Acc ([g]) ([ ⊢ B[]]) ([g ⊢ app M N]) r = sn in Acc [_] [_ ⊢ _] [_ ⊢ _] (mlam N' ⇒ mlam S ⇒ app_snb [_ ⊢ M] [_ ⊢ N'] (r [_ ⊢ app M N'] [_ ⊢ rappr S]));
rec inl_sn : (g:cxt) {M : [g ⊢ tm A[]]} {B : [ ⊢ ty]} Sn [g ⊢ M] → Sn [g ⊢ inl B[] M] / total sn ( inl_sn g a m b sn ) / =
mlam M ⇒ mlam B ⇒ fn sn ⇒
let Acc ([g]) ([ ⊢ A[]]) ([g ⊢ M]) r = sn in Acc [g] [ ⊢ sum A B] [g ⊢ inl B[] M] (mlam M' ⇒ mlam S ⇒
let [g ⊢ rinl S'] = [g ⊢ S] in inl_sn [_ ⊢ _] [ ⊢ B] (r [_ ⊢ _] [_ ⊢ S']));
rec inr_sn : (g:cxt) {M : [g ⊢ tm B[]]} {A : [ ⊢ ty]} Sn [g ⊢ M] → Sn [g ⊢ inr A[] M] / total sn ( inr_sn g b m a sn ) / =
mlam M ⇒ mlam A ⇒ fn sn ⇒
let Acc ([g]) ([ ⊢ B[]]) ([g ⊢ M]) r = sn in Acc [g] [ ⊢ sum A B] [g ⊢ inr A[] M] (mlam M' ⇒ mlam S ⇒
let [g ⊢ rinr S'] = [g ⊢ S] in inr_sn [_ ⊢ _] [ ⊢ A] (r [_ ⊢ _] [_ ⊢ S']));
rec case_sna : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ match M (λx. N1) (λy. N2)] → Sn [g ⊢ M] / total sn ( case_sna g a b c m n1 n2 sn ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn ⇒
let [_ ⊢ M] : [g ⊢ tm (sum A[] B[])]= [_ ⊢ M] in
let Acc ([g]) ([ ⊢ C]) ([g ⊢ match M (λx. N1) (λy. N2)]) r = sn in Acc [g] [ ⊢ sum A[] B[]] [g ⊢ M] (mlam M' ⇒ mlam S ⇒ case_sna [_ ⊢ M'] [_ ⊢ N1] [_ ⊢ N2] (r [_ ⊢ _] [_ ⊢ rcase S]));
rec case_snb : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ match M (λx. N1) (λy. N2)] → Sn [g, x : tm A[] ⊢ N1] / total sn ( case_snb g a b c m n1 n2 sn ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn ⇒
let [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in
let Acc ([g]) ([ ⊢ C]) ([g ⊢ match M (λx. N1) (λy. N2)]) r = sn in Acc [g, x : tm A[]] [ ⊢ C] [g, x : tm A[] ⊢ N1] (mlam N1' ⇒ mlam S ⇒ case_snb [_ ⊢ M] [_ ⊢ N1'] [_ ⊢ N2] (r [_ ⊢ _] [_ ⊢ rcl (λx. S)]));
rec case_snc : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ match M (λx. N1) (λy. N2)] → Sn [g, y : tm B[] ⊢ N2] / total sn ( case_snc g a b c m n1 n2 sn ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn ⇒
let [_ ⊢ N2] : [g, y : tm B[] ⊢ tm C[]]= [_ ⊢ N2] in
let Acc ([g]) ([ ⊢ C]) ([g ⊢ match M (λx. N1) (λy. N2)]) r = sn in Acc [g, y : tm B[]] [ ⊢ C] [g, y : tm B[] ⊢ N2] (mlam N2' ⇒ mlam S ⇒ case_snc [_ ⊢ M] [_ ⊢ N1] [_ ⊢ N2'] (r [_ ⊢ _] [_ ⊢ rcr (λy. S)]));
rec app_abs_sn : {g : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {M : [g, x : tm A[] ⊢ tm B[]]} {N : [g ⊢ tm A[]]} Sn [g ⊢ M[…, N]] → Sn [g ⊢ N] → Sn [g ⊢ app (abs (λx. M)) N] / total {sn2 sn1} ( app_abs_sn g a b m n sn1 sn2 ) / =
mlam g ⇒ mlam A ⇒ mlam B ⇒ mlam M ⇒ mlam N ⇒ fn sn1 ⇒ fn sn2 ⇒ Acc [g] [ ⊢ B] [g ⊢ app (abs (λx. M)) N] (mlam P ⇒ mlam S ⇒ case [_ ⊢ S] of
| [g ⊢ rbeta] ⇒ sn1
| [g ⊢ rappl S'] ⇒
let [_ ⊢ rabs (λx. S'')] = [_ ⊢ S'] in
let [_ ⊢ S''] : [g, x : tm _ ⊢ step M M']= [_ ⊢ S''] in
let [_ ⊢ S'''] = [_ ⊢ S''[…, N]] in
let Acc ([g]) ([ ⊢ B]) ([g ⊢ _]) r = sn1 in app_abs_sn [g] [ ⊢ _] [ ⊢ _] [_ ⊢ M'] [_ ⊢ N] (r [_ ⊢ M'[…, N]] [_ ⊢ S''']) sn2
| [g ⊢ rappr S'] ⇒
let Acc ([g]) ([ ⊢ A]) ([g ⊢ N]) r = sn2 in
let [_ ⊢ S'] : [_ ⊢ step N N']= [_ ⊢ S'] in
let [_ ⊢ MS''] = subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] [_ ⊢ S'] in
let sn' = mstep_sn [_ ⊢ M[…, N]] [_ ⊢ M[…, N']] [_ ⊢ MS''] sn1 in
app_abs_sn [g] [ ⊢ _] [ ⊢ _] [_ ⊢ M] [_ ⊢ N'] sn' (r [_ ⊢ N'] [_ ⊢ S']));
inductive Neutral : {g : cxt} → {M : [g ⊢ tm A[]]} → ctype =
| Nvar : {#x : [g ⊢ tm A[]]} Neutral [g ⊢ #x]
| Napp : {R : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Neutral [g ⊢ R] → Neutral [g ⊢ app R N]
| Ncase : {R : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Neutral [g ⊢ R] → Neutral [g ⊢ match R (λx. N1) (λy. N2)];
rec neu_step : (g:cxt) {R : [g ⊢ tm A[]]} {R' : [g ⊢ tm A[]]} [g ⊢ step R R'] → Neutral [g ⊢ R] → Neutral [g ⊢ R'] / total s ( neu_step g a r r' s n ) / =
mlam R ⇒ mlam R' ⇒ fn s ⇒ fn neu ⇒ case neu of
| Nvar ([g ⊢ #x]) ⇒ impossible s
| Napp ([g ⊢ R'']) ([g ⊢ N]) neu' ⇒
case s of
| [g ⊢ rbeta] ⇒ impossible neu'
| [g ⊢ rappl S'] ⇒
let neu'' = neu_step [_ ⊢ R''] [_ ⊢ _] [_ ⊢ S'] neu' in
Napp [_ ⊢ _] [_ ⊢ N] neu''
| [g ⊢ rappr S'] ⇒ Napp [_ ⊢ R''] [_ ⊢ _] neu'
| Ncase ([g ⊢ R'']) ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2]) neu' ⇒
case s of
| [g ⊢ rcase S'] ⇒
let neu'' = neu_step [_ ⊢ R''] [_ ⊢ _] [_ ⊢ S'] neu' in
Ncase [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] neu''
| [g ⊢ rcinl] ⇒ impossible neu'
| [g ⊢ rcinr] ⇒ impossible neu'
| [g ⊢ rcl (λx. S')] ⇒ Ncase [_ ⊢ R''] [_ ⊢ _] [_ ⊢ N2] neu'
| [g ⊢ rcr (λy. S')] ⇒ Ncase [_ ⊢ R''] [_ ⊢ N1] [_ ⊢ _] neu';
rec app_sn : {g : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {R : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Neutral [g ⊢ R] → Sn [g ⊢ R] → Sn [g ⊢ N] → Sn [g ⊢ app R N] / total {sn1 sn2} ( app_sn g a b r n neu sn1 sn2 ) / =
mlam g ⇒ mlam A ⇒ mlam B ⇒ mlam R ⇒ mlam N ⇒ fn neu ⇒ fn sn1 ⇒ fn sn2 ⇒ Acc [g] [ ⊢ B] [g ⊢ app R N] (mlam Q ⇒ mlam S ⇒ case [g ⊢ S] of
| [g ⊢ rbeta] ⇒ impossible neu
| [g ⊢ rappl S'] ⇒
let Acc ([g]) ([ ⊢ arr A B]) ([g ⊢ R]) r = sn1 in
let neu' = neu_step [_ ⊢ _] [_ ⊢ _] [_ ⊢ S'] neu in
app_sn [g] [ ⊢ A] [ ⊢ B] [g ⊢ _] [g ⊢ N] neu' (r [_ ⊢ _] [_ ⊢ S']) sn2
| [g ⊢ rappr S'] ⇒
let Acc ([g]) ([ ⊢ A]) ([g ⊢ N]) r = sn2 in app_sn [g] [ ⊢ A] [ ⊢ B] [_ ⊢ R] [_ ⊢ _] neu sn1 (r [_ ⊢ _] [_ ⊢ S']));
rec match_sn : (g:cxt) {R : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Neutral [g ⊢ R] → Sn [g ⊢ R] → Sn [g, x : tm A[] ⊢ N1] → Sn [g, y : tm B[] ⊢ N2] → Sn [g ⊢ match R (λx. N1) (λy. N2)] / total {sn0 sn1 sn2} ( match_sn g a b c r n1 n2 neu sn0 sn1 sn2 ) / =
mlam R ⇒ mlam N1 ⇒ mlam N2 ⇒ fn neu ⇒ fn sn0 ⇒ fn sn1 ⇒ fn sn2 ⇒
let [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in Acc [g] [ ⊢ C] [g ⊢ match R (λx. N1) (λy. N2)] (mlam M' ⇒ mlam S ⇒ case [g ⊢ S] of
| [g ⊢ rcase S'] ⇒
let Acc ([g]) ([ ⊢ sum A[] B[]]) ([g ⊢ R]) r = sn0 in
let neu' = neu_step [_ ⊢ _] [_ ⊢ _] [_ ⊢ S'] neu in
match_sn [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] neu' (r [_ ⊢ _] [_ ⊢ S']) sn1 sn2
| [g ⊢ rcinl] ⇒ impossible neu
| [g ⊢ rcinr] ⇒ impossible neu
| [g ⊢ rcl (λx. S')] ⇒
let Acc ([g, x : tm A[]]) ([ ⊢ C[]]) ([g, x : tm A[] ⊢ N1]) r = sn1 in match_sn [_ ⊢ R] [_ ⊢ _] [_ ⊢ N2] neu sn0 (r [_ ⊢ _] [_ ⊢ S']) sn2
| [g ⊢ rcr (λy. S')] ⇒
let Acc ([g, y : tm B[]]) ([ ⊢ C[]]) ([g, y : tm B[] ⊢ N2]) r = sn2 in match_sn [_ ⊢ R] [_ ⊢ N1] [_ ⊢ _] neu sn0 sn1 (r [_ ⊢ _] [_ ⊢ S']));
rec casel_sn : (g:cxt) {M : [g ⊢ tm A[]]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ M] → Sn [g ⊢ N1[…, M]] → Sn [g, y : tm B[] ⊢ N2] → Sn [g ⊢ match (inl B[] M) (λx. N1) (λy. N2)] / total {sn0 sn1 sn2} ( casel_sn g a b c m n1 n2 sn0 sn1 sn2 ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn0 ⇒ fn sn1 ⇒ fn sn2 ⇒
let [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in
let [_ ⊢ N2] : [g, y : tm B[] ⊢ tm C[]]= [_ ⊢ N2] in Acc [g] [ ⊢ C] [g ⊢ match (inl B[] M) (λx. N1) (λy. N2)] (mlam P ⇒ mlam S ⇒ case [g ⊢ S] of
| [g ⊢ rcase (rinl S')] ⇒
let Acc ([g]) ([ ⊢ A]) ([g ⊢ M]) r = sn0 in
let ms = subst_mred [_ ⊢ N1] [_ ⊢ M] [_ ⊢ _] [_ ⊢ S'] in
let sn1' = mstep_sn [_ ⊢ N1[…, M]] [_ ⊢ _] ms sn1 in
casel_sn [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] (r [_ ⊢ _] [_ ⊢ S']) sn1' sn2
| [g ⊢ rcinl] ⇒ sn1
| [g ⊢ rcl (λx. S')] ⇒
let [_ ⊢ S''] = [_ ⊢ S'[…, M]] in
let Acc ([g]) ([ ⊢ C]) ([g ⊢ _]) r = sn1 in casel_sn [_ ⊢ M] [_ ⊢ _] [_ ⊢ N2] sn0 (r [_ ⊢ _] [_ ⊢ S'']) sn2
| [g ⊢ rcr (λy. S')] ⇒
let Acc ([g, y : tm B[]]) ([ ⊢ C]) ([g, y : tm B[] ⊢ N2]) r = sn2 in casel_sn [_ ⊢ M] [_ ⊢ N1] [_ ⊢ _] sn0 sn1 (r [_ ⊢ _] [_ ⊢ S']));
rec caser_sn : (g:cxt) {M : [g ⊢ tm B[]]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ M] → Sn [g, x : tm A[] ⊢ N1] → Sn [g ⊢ N2[…, M]] → Sn [g ⊢ match (inr A[] M) (λx. N1) (λy. N2)] / total {sn0 sn1 sn2} ( caser_sn g b a c m n1 n2 sn0 sn1 sn2 ) / =
mlam M ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn0 ⇒ fn sn1 ⇒ fn sn2 ⇒
let [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in
let [_ ⊢ N2] : [g, y : tm B[] ⊢ tm C[]]= [_ ⊢ N2] in Acc [g] [ ⊢ C] [g ⊢ match (inr A[] M) (λx. N1) (λy. N2)] (mlam P ⇒ mlam S ⇒ case [g ⊢ S] of
| [g ⊢ rcase (rinr S')] ⇒
let Acc ([g]) ([ ⊢ B]) ([g ⊢ M]) r = sn0 in
let ms = subst_mred [g, x : tm B[] ⊢ N2] [g ⊢ M[…]] [g ⊢ _] [g ⊢ S'] in
let sn2' = mstep_sn [g ⊢ N2[…, M]] [g ⊢ _] ms sn2 in
caser_sn [g ⊢ _] [g, x : tm A[] ⊢ N1] [g, x : tm B[] ⊢ N2] (r [g ⊢ _] [g ⊢ S']) sn1 sn2'
| [g ⊢ rcinr] ⇒ sn2
| [g ⊢ rcl (λx. S')] ⇒
let Acc ([g, x : tm A[]]) ([ ⊢ C]) ([g, x : tm A[] ⊢ N1]) r = sn1 in caser_sn [_ ⊢ M] [_ ⊢ _] [_ ⊢ N2] sn0 (r [_ ⊢ _] [_ ⊢ S']) sn2
| [g ⊢ rcr (λy. S')] ⇒
let [_ ⊢ S''] = [_ ⊢ S'[…, M]] in
let Acc ([g]) ([ ⊢ C]) ([g ⊢ _]) r = sn2 in caser_sn [_ ⊢ M] [_ ⊢ N1] [_ ⊢ _] sn0 sn1 (r [_ ⊢ _] [_ ⊢ S'']));
inductive ConfResult : {g : cxt} → {N : [g ⊢ tm A[]]} → {N' : [g ⊢ tm A[]]} → ctype =
| Eq : ConfResult [g ⊢ N] [g ⊢ N]
| Conf : SnRed [g ⊢ N'] [g ⊢ Q] → [g ⊢ mstep N Q] → ConfResult [g ⊢ N] [g ⊢ N'];
rec confluence : (g:cxt) {M : [g ⊢ tm A[]]} {N : [g ⊢ tm A[]]} {N' : [g ⊢ tm A[]]} {S : [g ⊢ step M N']} SnRed [g ⊢ M] [g ⊢ N] → ConfResult [g ⊢ N] [g ⊢ N'] / total s ( confluence g a m n n' s ) / =
mlam M ⇒ mlam N ⇒ mlam N' ⇒ mlam S ⇒ fn snr ⇒ case snr of
| SnBeta ([g, x : tm A[] ⊢ M]) sn ⇒
case [g ⊢ S] of
| [g ⊢ rbeta] ⇒ Eq
| [g ⊢ rappl S'] ⇒
let [_ ⊢ rabs (λx. S'')] = [_ ⊢ S'] in
let [_ ⊢ S''] : [g, x : tm _ ⊢ step M M']= [_ ⊢ S''] in
let snr' = SnBeta [g, x : tm _ ⊢ M'] sn in
let sn : Sn [g ⊢ N]= sn in
let [_ ⊢ R] = [_ ⊢ S''[…, N]] in Conf snr' [g ⊢ m-step R m-refl]
| [g ⊢ rappr S'] ⇒
let [_ ⊢ S'] : [_ ⊢ step N N']= [_ ⊢ S'] in
let ms = subst_mred [_ ⊢ M] [_ ⊢ N] [_ ⊢ N'] [_ ⊢ S'] in
let Acc ([_]) ([ ⊢ _]) ([_ ⊢ _]) r = sn in
let sn' = r [_ ⊢ N'] [_ ⊢ S'] in Conf (SnBeta [g, x : tm _ ⊢ M] sn') ms
| SnAppl r ⇒
case [_ ⊢ S] of
| [g ⊢ rbeta] ⇒ impossible r
| [g ⊢ rappl S'] ⇒
let conf = confluence [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ S'] r in
case conf of
| Eq ⇒ Eq
| Conf snr' ms ⇒
let snr' : SnRed [g ⊢ M2] [g ⊢ P]= snr' in
let ms' = mstep_appl [_ ⊢ _] [_ ⊢ P] [_ ⊢ _] ms in
Conf (SnAppl snr') ms'
| [g ⊢ rappr S'] ⇒
let ms = [_ ⊢ m-step S' m-refl] in
let r : SnRed [_ ⊢ M] [_ ⊢ M']= r in
let ms' = mstep_appr [_ ⊢ M'] [_ ⊢ _] [_ ⊢ _] ms in
Conf (SnAppl r) ms'
| SnCInl sn sn1 sn2 ⇒
let Acc ([g]) ([ ⊢ sum A1[] A2[]]) ([g ⊢ M0]) r = sn in case [g ⊢ S] of
| [g ⊢ rcase (rinl S')] ⇒
let sn' = r [_ ⊢ _] [_ ⊢ S'] in
let snr' = SnCInl sn' sn1 sn2 in
let Acc ([_]) ([ ⊢ _]) ([_ ⊢ N1]) r = sn1 in
let ms = subst_mred [_ ⊢ N1] [_ ⊢ M0] [_ ⊢ _] [_ ⊢ S'] in Conf snr' ms
| [g ⊢ rcinl] ⇒ Eq
| [g ⊢ rcl (λx. S')] ⇒
let [_ ⊢ S'] : [g, x : tm _ ⊢ step N1 N1']= [_ ⊢ S'] in
let [_ ⊢ S''] = [_ ⊢ S'[…, M0]] in
let Acc ([g, x : tm A[]]) ([ ⊢ C]) ([g, x : tm A[] ⊢ N1]) r = sn1 in
let sn1' = r [_ ⊢ N1'] [_ ⊢ S'] in
let snr' = SnCInl sn sn1' sn2 in
Conf snr' [g ⊢ m-step S'' m-refl]
| [g ⊢ rcr (λy. S')] ⇒
let Acc ([g, y : tm A2[]]) ([ ⊢ C[]]) ([g, y : tm A2[] ⊢ N2]) r' = sn2 in
let sn2' = r' [_ ⊢ _] [_ ⊢ S'] in
let snr' = SnCInl sn sn1 sn2' in Conf snr' [g ⊢ m-refl]
| SnCInr sn sn1 sn2 ⇒
let Acc ([g]) ([ ⊢ sum A1[] A2[]]) ([g ⊢ M0]) r = sn in case [g ⊢ S] of
| [g ⊢ rcase (rinr S')] ⇒
let sn' = r [_ ⊢ _] [_ ⊢ S'] in
let Acc ([_]) ([ ⊢ _]) ([_ ⊢ N2]) r = sn2 in
let snr' = SnCInr sn' sn1 sn2 in
let ms = subst_mred [_ ⊢ N2] [_ ⊢ M0] [_ ⊢ _] [_ ⊢ S'] in Conf snr' ms
| [g ⊢ rcinr] ⇒ Eq
| [g ⊢ rcl (λx. S')] ⇒
let Acc ([g, x : tm A1[]]) ([ ⊢ C[]]) ([g, x : tm A1[] ⊢ N1]) r' = sn1 in
let sn1' = r' [_ ⊢ _] [_ ⊢ S'] in
let Acc ([_]) ([ ⊢ _]) ([_ ⊢ N2]) r = sn2 in
let snr' = SnCInr sn sn1' sn2 in Conf snr' [g ⊢ m-refl]
| [g ⊢ rcr (λx. S')] ⇒
let [_ ⊢ S'] : [g, x : tm _ ⊢ step N2 N2']= [_ ⊢ S'] in
let [_ ⊢ S''] = [_ ⊢ S'[…, M0]] in
let Acc ([g, y : tm B[]]) ([ ⊢ C]) ([g, y : tm B[] ⊢ N2]) r = sn2 in
let sn2' = r [_ ⊢ N2'] [_ ⊢ S'] in
let snr' = SnCInr sn sn1 sn2' in
Conf snr' [g ⊢ m-step S'' m-refl]
| SnCasR snr' ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2]) ⇒
case [g ⊢ S] of
| [g ⊢ rcase S'] ⇒
let conf = confluence [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ S'] snr' in
case conf of
| Eq ⇒ Eq
| Conf snr'' ms ⇒
let [_ ⊢ MS] = mstep_match [_ ⊢ _] [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] ms in Conf (SnCasR snr'' [_ ⊢ N1] [_ ⊢ N2]) [_ ⊢ MS]
| [g ⊢ rcinl] ⇒ impossible snr'
| [g ⊢ rcinr] ⇒ impossible snr'
| [g ⊢ rcl (λx. S')] ⇒
let [_ ⊢ S'] : [g, x : tm _ ⊢ step N1 N1']= [_ ⊢ S'] in
let snr'' = SnCasR snr' [_ ⊢ N1'] [_ ⊢ N2] in
let snr' : SnRed [g ⊢ M] [g ⊢ M']= snr' in
let ms =
mstep_matchl [_ ⊢ N1] [_ ⊢ N1'] [_ ⊢ M'] [_ ⊢ N2] [_ ⊢ m-step S' m-refl] in
Conf snr'' ms
| [g ⊢ rcr (λy. S')] ⇒
let [_ ⊢ S'] : [g, x : tm _ ⊢ step N2 N2']= [_ ⊢ S'] in
let snr'' = SnCasR snr' [_ ⊢ N1] [_ ⊢ N2'] in
let snr' : SnRed [g ⊢ M] [g ⊢ M']= snr' in
let ms =
mstep_matchr [_ ⊢ N2] [_ ⊢ N2'] [_ ⊢ M'] [_ ⊢ N1] [_ ⊢ m-step S' m-refl] in
Conf snr'' ms;
rec bc_aux_app : {g : cxt} {A : [ ⊢ ty]} {B : [ ⊢ ty]} {M : [g ⊢ tm (arr A[] B[])]} {M' : [g ⊢ tm (arr A[] B[])]} {N : [g ⊢ tm A[]]} Sn [g ⊢ M] → Sn [g ⊢ N] → SnRed [g ⊢ M] [g ⊢ M'] → Sn [g ⊢ app M' N] → Sn [g ⊢ app M N] / total {sn1 sn2} ( bc_aux_app g a b m m' n sn1 sn2 ) / =
mlam g ⇒ mlam A ⇒ mlam B ⇒ mlam M ⇒ mlam M' ⇒ mlam N ⇒ fn sn1 ⇒ fn sn2 ⇒ fn snr ⇒ fn sn ⇒ Acc [g] [ ⊢ B] [g ⊢ app M N] (mlam Q ⇒ mlam S ⇒ case [g ⊢ S] of
| [g ⊢ rbeta] ⇒ impossible snr
| [g ⊢ rappl S'] ⇒
let conf = confluence [_ ⊢ M] [_ ⊢ M'] [_ ⊢ _] [_ ⊢ S'] snr in
case conf of
| Eq ⇒ sn
| Conf snr' ms ⇒
let ms' = mstep_appl [_ ⊢ M'] [_ ⊢ _] [_ ⊢ N] ms in
let sn' = mstep_sn [_ ⊢ app M' N] [_ ⊢ _] ms' sn in
let Acc ([g]) ([ ⊢ arr A B]) ([g ⊢ M]) r = sn1 in bc_aux_app [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ N] (r [_ ⊢ _] [_ ⊢ S']) sn2 snr' sn'
| [g ⊢ rappr S'] ⇒
let Acc ([g]) ([ ⊢ B]) ([g ⊢ app M' N]) r = sn in
let sn' = r [_ ⊢ _] [_ ⊢ rappr S'] in
let Acc ([g]) ([ ⊢ A]) ([g ⊢ N]) r' = sn2 in bc_aux_app [_] [ ⊢ _] [ ⊢ _] [_ ⊢ M] [_ ⊢ M'] [_ ⊢ _] sn1 (r' [_ ⊢ _] [_ ⊢ S']) snr sn');
rec bc_aux_sum : (g:cxt) {M : [g ⊢ tm (sum A[] B[])]} {M' : [g ⊢ tm (sum A[] B[])]} {N1 : [g, x : tm A[] ⊢ tm C[]]} {N2 : [g, y : tm B[] ⊢ tm C[]]} Sn [g ⊢ M] → Sn [g, x : tm A[] ⊢ N1] → Sn [g, y : tm B[] ⊢ N2] → SnRed [g ⊢ M] [g ⊢ M'] → Sn [g ⊢ match M' (λx. N1) (λy. N2)] → Sn [g ⊢ match M (λx. N1) (λy. N2)] / total {sn0 sn1 sn2} ( bc_aux_sum g a b c m m' n1 n2 sn0 sn1 sn2 ) / =
mlam M ⇒ mlam M' ⇒ mlam N1 ⇒ mlam N2 ⇒ fn sn0 ⇒ fn sn1 ⇒ fn sn2 ⇒ fn snr ⇒ fn sn' ⇒
let [_ ⊢ N1] : [g, x : tm A[] ⊢ tm C[]]= [_ ⊢ N1] in Acc [g] [ ⊢ C] [g ⊢ match M (λx. N1) (λy. N2)] (mlam Q ⇒ mlam S ⇒ case [g ⊢ S] of
| [g ⊢ rcase S'] ⇒
let conf = confluence [_ ⊢ M] [_ ⊢ M'] [_ ⊢ _] [_ ⊢ S'] snr in
case conf of
| Eq ⇒ sn'
| Conf snr' ms ⇒
let [_ ⊢ MS] = mstep_match [_ ⊢ M'] [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] ms in
let sn'' = mstep_sn [_ ⊢ _] [_ ⊢ _] [_ ⊢ MS] sn' in
let Acc ([g]) ([ ⊢ _]) ([g ⊢ M]) r = sn0 in bc_aux_sum [_ ⊢ _] [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] (r [_ ⊢ _] [_ ⊢ S']) sn1 sn2 snr' sn''
| [g ⊢ rcinl] ⇒ impossible snr
| [g ⊢ rcinr] ⇒ impossible snr
| [g ⊢ rcl (λx. S')] ⇒
let [_ ⊢ S'] : [g, x : tm _ ⊢ step N1 N1']= [_ ⊢ S'] in
let Acc ([g]) ([ ⊢ _]) ([g ⊢ _]) r = sn' in
let sn'' = r [g ⊢ match M' (λx. N1') (λy. N2)] [g ⊢ rcl (λx. S')] in
let Acc ([g, x : tm _]) ([ ⊢ C]) ([g, x : tm _ ⊢ N1]) r' = sn1 in bc_aux_sum [_ ⊢ M] [_ ⊢ M'] [_ ⊢ N1'] [_ ⊢ N2] sn0 (r' [_ ⊢ N1'] [_ ⊢ S']) sn2 snr sn''
| [g ⊢ rcr (λy. S')] ⇒
let [_ ⊢ S'] : [g, y : tm _ ⊢ step N2 N2']= [_ ⊢ S'] in
let Acc ([g]) ([ ⊢ _]) ([g ⊢ _]) r = sn' in
let sn'' = r [g ⊢ match M' (λx. N1) (λy. N2')] [g ⊢ rcr (λy. S')] in
let Acc ([g, y : tm _]) ([ ⊢ C]) ([g, y : tm _ ⊢ N2]) r' = sn2 in bc_aux_sum [_ ⊢ M] [_ ⊢ M'] [_ ⊢ N1] [_ ⊢ N2'] sn0 sn1 (r' [_ ⊢ N2'] [_ ⊢ S']) snr sn'');
rec backwards_closure : (g:cxt) {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} SnRed [g ⊢ M] [g ⊢ M'] → Sn [g ⊢ M'] → Sn [g ⊢ M] / total r ( backwards_closure g a m m' r ) / =
mlam M ⇒ mlam M' ⇒ fn snr ⇒ fn sn ⇒ case snr of
| SnBeta ([g, x : tm A[] ⊢ M]) sn' ⇒ app_abs_sn [_] [ ⊢ _] [ ⊢ _] [_ ⊢ M] [_ ⊢ _] sn sn'
| SnAppl r ⇒
let snl' = app_sna [_ ⊢ _] [_ ⊢ _] sn in
let snl = backwards_closure [_ ⊢ _] [_ ⊢ _] r snl' in
let snr = app_snb [_ ⊢ _] [_ ⊢ _] sn in
bc_aux_app [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] snl snr r sn
| SnCInl sn0 sn1 sn2 ⇒ casel_sn [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] sn0 sn sn2
| SnCInr sn0 sn1 sn2 ⇒ caser_sn [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] sn0 sn1 sn
| SnCasR snr' ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2]) ⇒
let sn' = case_sna [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] sn in
let sn0 = backwards_closure [_ ⊢ _] [_ ⊢ _] snr' sn' in
let sn1 = case_snb [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] sn in
let sn2 = case_snc [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] sn in
bc_aux_sum [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] sn0 sn1 sn2 snr' sn;
rec neutralSNe : (g:cxt) {R : [g ⊢ tm A[]]} SNe [g ⊢ R] → Neutral [g ⊢ R] / total sne ( neutralSNe g a r sne ) / =
mlam R ⇒ fn sne ⇒ case sne of
| SVar ([g ⊢ #p]) ⇒ Nvar [g ⊢ #p]
| SApp sne' sn ⇒
let neu = neutralSNe [_ ⊢ _] sne' in Napp [_ ⊢ _] [_ ⊢ _] neu
| SCase sne' sn1 sn2 ⇒
let neu = neutralSNe [_ ⊢ _] sne' in
let sn1 : SN [g, x : tm A[] ⊢ N1]= sn1 in
let sn2 : SN [g, x : tm B[] ⊢ N2]= sn2 in Ncase [_ ⊢ _] [_ ⊢ N1] [_ ⊢ N2] neu;
rec soundSN : (g:cxt) {M : [g ⊢ tm A[]]} SN [g ⊢ M] → Sn [g ⊢ M] / total s ( soundSN g a m s ) / =
mlam M ⇒ fn sn ⇒ case sn of
| SNeu sne ⇒ soundSNe [_ ⊢ M] sne
| SAbs sn' ⇒
let sn'' = soundSN [_ ⊢ _] sn' in abs_sn [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] sn''
| SRed snr sn' ⇒
let snr' = soundSNRed [_ ⊢ _] [_ ⊢ _] snr in
let sn'' = soundSN [_ ⊢ _] sn' in backwards_closure [_ ⊢ M] [_ ⊢ _] snr' sn''
| SInl sn' ⇒
let sn'' = soundSN [_ ⊢ _] sn' in inl_sn [_ ⊢ _] [ ⊢ _] sn''
| SInr sn' ⇒
let sn'' = soundSN [_ ⊢ _] sn' in inr_sn [_ ⊢ _] [ ⊢ _] sn''
and soundSNe : (g:cxt) {M : [g ⊢ tm A[]]} SNe [g ⊢ M] → Sn [g ⊢ M] / total s ( soundSNe g a m s ) / =
mlam M ⇒ fn sne ⇒ case sne of
| SVar ([g ⊢ #p]) ⇒ varSn [g ⊢ #p]
| SApp sne' sn ⇒
let snl = soundSNe [_ ⊢ _] sne' in
let snr = soundSN [_ ⊢ _] sn in
let neu = neutralSNe [_ ⊢ _] sne' in
app_sn [_] [ ⊢ _] [ ⊢ _] [_ ⊢ _] [_ ⊢ _] neu snl snr
| SCase sne' snl snr ⇒
let neu = neutralSNe [_ ⊢ _] sne' in
let sn0 = soundSNe [_ ⊢ _] sne' in
let sn1 = soundSN [_ ⊢ _] snl in
let sn2 = soundSN [_ ⊢ _] snr in match_sn [_ ⊢ _] [_ ⊢ _] [_ ⊢ _] neu sn0 sn1 sn2
and soundSNRed : (g:cxt) {M : [g ⊢ tm A[]]} {M' : [g ⊢ tm A[]]} SNRed [g ⊢ M] [g ⊢ M'] → SnRed [g ⊢ M] [g ⊢ M'] / total s ( soundSNRed g a m m' s ) / =
mlam M ⇒ mlam M' ⇒ fn snr ⇒ case snr of
| SBeta ([g, x : tm A[] ⊢ M]) sn ⇒
let sn' = soundSN [_ ⊢ _] sn in SnBeta [_ ⊢ M] sn'
| SAppl snr' ⇒
let snr'' = soundSNRed [_ ⊢ _] [_ ⊢ _] snr' in SnAppl snr''
| SCInl sn0 sn1 sn2 ⇒
let sn0' = soundSN [_ ⊢ _] sn0 in
let sn1' = soundSN [_ ⊢ _] sn1 in
let sn2' = soundSN [_ ⊢ _] sn2 in SnCInl sn0' sn1' sn2'
| SCInr sn0 sn1 sn2 ⇒
let sn0' = soundSN [_ ⊢ _] sn0 in
let sn1' = soundSN [_ ⊢ _] sn1 in
let sn2' = soundSN [_ ⊢ _] sn2 in SnCInr sn0' sn1' sn2'
| SRCase snr' ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2]) ⇒
let snr'' = soundSNRed [_ ⊢ _] [_ ⊢ _] snr' in SnCasR snr'' [_ ⊢ N1] [_ ⊢ N2];
rec renameSN : {g : cxt} {g' : cxt} [g' ⊢ g] {M : [g ⊢ tm A[]]} SN [g ⊢ M] → SN [g' ⊢ M[#R]] / total s ( renameSN g g' a r m s ) / =
mlam g ⇒ mlam g' ⇒ mlam R ⇒ mlam M ⇒ fn s ⇒ case s of
| SNeu s' ⇒ SNeu (renameSNe [g' ⊢ #R] [g ⊢ M] s')
| SAbs s' ⇒
SAbs (renameSN [g, x : tm _] [g', x : tm _] [g', x : tm _ ⊢ #R[…], x] [g, x : tm _ ⊢ _] s')
| SRed r s' ⇒ SRed (renameSNRed [g' ⊢ #R] [g ⊢ M] r) (renameSN [g] [g'] [g' ⊢ #R] [g ⊢ _] s')
| SInl s' ⇒ SInl (renameSN [g] [g'] [g' ⊢ #R] [g ⊢ _] s')
| SInr s' ⇒ SInr (renameSN [g] [g'] [g' ⊢ #R] [g ⊢ _] s')
and renameSNe : (g:cxt) (g':cxt) [g' ⊢ g] {M : [g ⊢ tm A[]]} SNe [g ⊢ M] → SNe [g' ⊢ M[#R]] / total s ( renameSNe g g' a r m s ) / =
mlam R ⇒ mlam M ⇒ fn s ⇒ case s of
| SVar ([g ⊢ #p]) ⇒ SVar [_ ⊢ #p[#R]]
| SApp s1 s2 ⇒
SApp (renameSNe [_ ⊢ #R] [_ ⊢ _] s1) (renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s2)
| SCase s1 s2 s3 ⇒
SCase (renameSNe [_ ⊢ #R] [_ ⊢ _] s1) (renameSN [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ #R[…], x] [_, x : tm _ ⊢ _] s2) (renameSN [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ #R[…], y] [_, y : tm _ ⊢ _] s3)
and renameSNRed : (g:cxt) (g':cxt) [g' ⊢ g] {M : [g ⊢ tm A[]]} SNRed [g ⊢ M] [g ⊢ N] → SNRed [g' ⊢ M[#R]] [g' ⊢ N[#R]] / total s ( renameSNRed g g' a r m s ) / =
mlam R ⇒ mlam M ⇒ fn s ⇒ case s of
| SBeta ([g, x : tm A[] ⊢ M]) s' ⇒
SBeta [_, x : tm A[] ⊢ M[#R[…], x]] (renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s')
| SAppl s' ⇒ SAppl (renameSNRed [_ ⊢ #R] [_ ⊢ _] s')
| SCInl s' n1 n2 ⇒
SCInl (renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s') (renameSN [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ #R[…], x] [_, x : tm _ ⊢ _] n1) (renameSN [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ #R[…], y] [_, y : tm _ ⊢ _] n2)
| SCInr s' n1 n2 ⇒
SCInr (renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s') (renameSN [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ #R[…], x] [_, x : tm _ ⊢ _] n1) (renameSN [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ #R[…], y] [_, y : tm _ ⊢ _] n2)
| SRCase s' ([g, x : tm A[] ⊢ N1]) ([g, y : tm B[] ⊢ N2]) ⇒
SRCase (renameSNRed [_ ⊢ #R] [_ ⊢ _] s') [_, x : tm A[] ⊢ N1[#R[…], x]] [_, y : tm B[] ⊢ N2[#R[…], y]];
inductive SNRed' : {g : cxt} → {g' : cxt} → [g' ⊢ g] → {M : [g ⊢ tm A[]]} → {M' : [g' ⊢ tm A[]]} → ctype =
| SNRed' : {g' : cxt} {g : cxt} {N : [g ⊢ tm A[]]} SNRed [g ⊢ M] [g ⊢ N] → SNRed' [g' ⊢ #R] [g ⊢ M] [g' ⊢ N[#R]];
rec anti_renameSNe : (g:cxt) (g':cxt) [g' ⊢ g] {M : [g ⊢ tm A[]]} SNe [g' ⊢ M[#R]] → SNe [g ⊢ M] / total s ( anti_renameSNe g g' a r m s ) / =
mlam R ⇒ mlam N ⇒ fn s ⇒ case s of
| SVar ([h' ⊢ _]) ⇒ SVar [_ ⊢ _]
| SApp r s ⇒
let r' = anti_renameSNe [_ ⊢ #R] [_ ⊢ _] r in
let s' = anti_renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s in SApp r' s'
| SCase s1 s2 s3 ⇒
let s1' = anti_renameSNe [_ ⊢ #R] [_ ⊢ _] s1 in
let s2' =
anti_renameSN [_, x : tm _] [_, x : tm _] [_, x : tm _ ⊢ #R[…], x] [_ ⊢ _] s2 in
let s3' =
anti_renameSN [_, y : tm _] [_, y : tm _] [_, y : tm _ ⊢ #R[…], y] [_ ⊢ _] s3 in
SCase s1' s2' s3'and anti_renameSNRed : {g : cxt} {g' : cxt} [g' ⊢ g] {M : [g ⊢ tm A[]]} SNRed [g' ⊢ M[#R]] [g' ⊢ N'] → SNRed' [g' ⊢ #R] [g ⊢ M] [g' ⊢ N'] / total s ( anti_renameSNRed g g' a r m s ) / =
mlam g ⇒ mlam g' ⇒ mlam R ⇒ mlam M ⇒ fn r ⇒ case r of
| SBeta ([_ ⊢ _]) s ⇒
let s' = anti_renameSN [g] [g'] [g' ⊢ #R] [_ ⊢ _] s in
SNRed' [_] [_] [_ ⊢ _] (SBeta [_ ⊢ _] s')
| SAppl r' ⇒
let SNRed' ([_]) ([_]) ([_ ⊢ _]) r0 =
anti_renameSNRed [g] [g'] [g' ⊢ #R] [_ ⊢ _] r' in SNRed' [_] [_] [_ ⊢ _] (SAppl r0)
| SCInl s n1 n2 ⇒
let s' = anti_renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s in
let s1 = anti_renameSN [g, x : tm _] [_] [g', x : tm _ ⊢ #R[…], x] [_ ⊢ _] n1 in
let s2 = anti_renameSN [g, y : tm _] [_] [g', y : tm _ ⊢ #R[…], y] [_ ⊢ _] n2 in
SNRed' [_] [_] [_ ⊢ _] (SCInl s' s1 s2)
| SCInr s n1 n2 ⇒
let s' = anti_renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s in
let s1 = anti_renameSN [g, x : tm _] [_] [g', x : tm _ ⊢ #R[…], x] [_ ⊢ _] n1 in
let s2 = anti_renameSN [g, y : tm _] [_] [g', y : tm _ ⊢ #R[…], y] [_ ⊢ _] n2 in
SNRed' [_] [_] [_ ⊢ _] (SCInr s' s1 s2)
| SRCase s ([g', x : tm _ ⊢ _]) ([g', y : tm _ ⊢ _]) ⇒
let SNRed' ([_]) ([_]) ([_ ⊢ _]) s' = anti_renameSNRed [_] [_] [_ ⊢ #R] [_ ⊢ _] s in SNRed' [_] [_] [_ ⊢ _] (SRCase s' [g, x : tm _ ⊢ _] [g, y : tm _ ⊢ _])
and anti_renameSN : {g : cxt} {g' : cxt} [g' ⊢ g] {M : [g ⊢ tm A[]]} SN [g' ⊢ M[#R]] → SN [g ⊢ M] / total s ( anti_renameSN g g' a r m s ) / =
mlam g ⇒ mlam g' ⇒ mlam R ⇒ mlam M ⇒ fn s ⇒ case s of
| SAbs s' ⇒
SAbs (anti_renameSN [g, x : tm _] [g', x : tm _] [g', x : tm _ ⊢ #R[…], x] [g, x : tm _ ⊢ _] s')
| SNeu s' ⇒ SNeu (anti_renameSNe [g' ⊢ #R] [g ⊢ M] s')
| SRed r' s' ⇒
let SNRed' ([g']) ([g]) ([g ⊢ N]) r =
anti_renameSNRed [_] [_] [g' ⊢ #R] [_ ⊢ _] r' in
let s'' = anti_renameSN [g] [g'] [g' ⊢ #R] [g ⊢ N] s' in SRed r s''
| SInl s' ⇒ SInl (anti_renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s')
| SInr s' ⇒ SInr (anti_renameSN [_] [_] [_ ⊢ #R] [_ ⊢ _] s');
rec ext_SN : {M : [g ⊢ tm (arr A[] B[])]} {#p : [g ⊢ tm A[]]} SN [g ⊢ app M (#p)] → SN [g ⊢ M] / total s ( ext_SN g a b m p s ) / =
mlam M ⇒ mlam p ⇒ fn s ⇒ case s of
| SNeu (SApp sm sv ) ⇒ SNeu sm
| SRed r sm' ⇒
case r of
| SBeta ([g, x : tm A[] ⊢ M']) sn ⇒
let sn' =
anti_renameSN [g, x : tm A[]] [g] [g ⊢ …, (#p[…])] [g, x : tm A[] ⊢ M'] sm' in
SAbs sn'
| SAppl r' ⇒ let sn = ext_SN [_ ⊢ _] [_ ⊢ #p] sm' in SRed r' sn;