Set Implicit Arguments.
Require Import RelationClasses Morphisms List
Omega Init.Nat Setoid std calculus unification.
Require Import third_order.pcp third_order.encoding.
Import ListNotations.
Require Import RelationClasses Morphisms List
Omega Init.Nat Setoid std calculus unification.
Require Import third_order.pcp third_order.encoding.
Import ListNotations.
Section HuetReduction.
Variable (X: Const).
Let v n: fin := n.
Let u n: fin := (S n).
Let h: exp X := var 0.
Let f: exp X := var 3.
Let g: exp X := var 4.
Variable (X: Const).
Let v n: fin := n.
Let u n: fin := (S n).
Let h: exp X := var 0.
Let f: exp X := var 3.
Let g: exp X := var 4.
Program Instance PCP_to_U (S: list card) : orduni 3 X :=
{
Gamma₀ := [Arr (repeat (alpha → alpha) (length S)) alpha; (alpha → alpha) → alpha];
s₀ := lambda lambda lambda h (AppR f (Enc 1 2 (heads S))) (AppR f (repeat (var (u 1)) (length S)));
t₀ := lambda lambda lambda h (AppR f (Enc 1 2 (tails S))) (var (u 1) (g (var (u 1))));
A₀ := (alpha → alpha) → (alpha → alpha) → (alpha → alpha → alpha) → alpha;
H1₀ := _;
H2₀ := _;
}.
Next Obligation with cbn; eauto.
do 4 econstructor. econstructor. econstructor; cbn; eauto; cbn; eauto.
- eapply AppR_ordertyping with (L := repeat (alpha → alpha) (length S) ); simplify.
erewrite <-map_length; eapply Enc_typing.
all: econstructor; eauto...
simplify; cbn; eauto.
- eapply AppR_ordertyping.
+ eapply repeated_ordertyping; simplify; eauto.
intros s H'. eapply repeated_in in H'. subst.
econstructor; cbn. 2: eauto. eauto...
+ econstructor; simplify; eauto...
Qed.
Next Obligation with cbn [ord' ord alpha]; simplify; cbn; eauto.
do 4 econstructor. econstructor. econstructor; eauto...
cbn; eauto.
2: do 2 econstructor...
2 - 3: econstructor...
eapply AppR_ordertyping with (L := repeat (alpha → alpha) (length S)); simplify; eauto.
erewrite <-map_length; eapply Enc_typing.
all: econstructor...
Qed.
Section ForwardDirection.
Definition ginst (I: list nat) : exp X :=
lambda AppL (repeat (var 0) (pred (|I|))) (var 1).
{
Gamma₀ := [Arr (repeat (alpha → alpha) (length S)) alpha; (alpha → alpha) → alpha];
s₀ := lambda lambda lambda h (AppR f (Enc 1 2 (heads S))) (AppR f (repeat (var (u 1)) (length S)));
t₀ := lambda lambda lambda h (AppR f (Enc 1 2 (tails S))) (var (u 1) (g (var (u 1))));
A₀ := (alpha → alpha) → (alpha → alpha) → (alpha → alpha → alpha) → alpha;
H1₀ := _;
H2₀ := _;
}.
Next Obligation with cbn; eauto.
do 4 econstructor. econstructor. econstructor; cbn; eauto; cbn; eauto.
- eapply AppR_ordertyping with (L := repeat (alpha → alpha) (length S) ); simplify.
erewrite <-map_length; eapply Enc_typing.
all: econstructor; eauto...
simplify; cbn; eauto.
- eapply AppR_ordertyping.
+ eapply repeated_ordertyping; simplify; eauto.
intros s H'. eapply repeated_in in H'. subst.
econstructor; cbn. 2: eauto. eauto...
+ econstructor; simplify; eauto...
Qed.
Next Obligation with cbn [ord' ord alpha]; simplify; cbn; eauto.
do 4 econstructor. econstructor. econstructor; eauto...
cbn; eauto.
2: do 2 econstructor...
2 - 3: econstructor...
eapply AppR_ordertyping with (L := repeat (alpha → alpha) (length S)); simplify; eauto.
erewrite <-map_length; eapply Enc_typing.
all: econstructor...
Qed.
Section ForwardDirection.
Definition ginst (I: list nat) : exp X :=
lambda AppL (repeat (var 0) (pred (|I|))) (var 1).
Lemma ginst_typing I:
[alpha] ⊢(3) ginst I : (alpha → alpha) → alpha.
Proof.
econstructor. eapply AppL_ordertyping_repeated.
eapply repeated_ordertyping.
intros ? ? % repeated_in; subst; eauto.
simplify; eauto.
econstructor; eauto.
Qed.
Lemma ginst_equivalence I (S: stack):
I <> nil -> I ⊆ nats (length S) ->
AppR (ren (add 3) (finst I (length S)))
(repeat (var (u 1)) (| S |)) ≡ var (u 1) (ren (add 3) (ginst I) (var (u 1))).
Proof.
intros H H0. unfold finst. rewrite !Lambda_ren, !AppL_ren.
rewrite !map_id_list.
2: intros ? ?; mapinj; cbn; eapply H0, nats_lt in H3; now rewrite it_up_ren_lt.
rewrite AppR_Lambda'; simplify; eauto.
unfold ginst; cbn [ren]; erewrite stepBeta.
2: asimpl; simplify; cbn; unfold funcomp; eauto.
cbn [ren]. rewrite it_up_ren_ge; simplify; eauto.
asimpl. rewrite select_variables_subst; simplify; eauto.
rewrite select_repeated; eauto.
unfold ginst; cbn; asimpl; simplify.
rewrite sapp_ge_in; simplify; eauto.
replace (_ - _) with 3 by omega.
destruct I; intuition.
Qed.
Lemma PCP_MU S:
PCP S -> OU 3 X (PCP_to_U S).
Proof.
intros (I & ? & ? & ?).
pose (sigma := finst I (length S) .: ginst I .: var).
exists [alpha]. exists sigma. split.
- intros x A. destruct x as [| [| x]]; try discriminate; cbn.
3: intros [] % nth_error_In.
all: injection 1 as ?; subst.
eapply finst_typing; eauto.
eapply ginst_typing.
- cbn -[ginst]. do 3 eapply equiv_lam_proper.
eapply equiv_app_proper.
eapply equiv_app_proper. reflexivity.
all: unfold shift, var_zero.
all: rewrite !AppR_subst; rewrite ?Enc_subst_id; eauto.
2: rewrite map_id_list.
3: intros ? ? % repeated_in; subst; reflexivity.
all: cbn; rewrite !ren_plus_base, !ren_plus_combine;
change (1 + 1 + 1) with 3.
2: rewrite !AppL_ren; simplify; cbn [ren]; unfold upRen_exp_exp.
2: unfold up_ren, funcomp; cbn [scons].
replace (|S|) with (|heads S|) at 1 by now simplify.
replace (|S|) with (|tails S|) at 1 by now simplify.
rewrite !finst_equivalence, H1; simplify; eauto.
rewrite ginst_equivalence; eauto.
unfold ginst; asimpl. now simplify.
Qed.
End ForwardDirection.
Section BackwardDirection.
Variables (s t: exp X) (x: nat) (sigma: fin -> exp X) (S: list (exp X)).
Hypothesis (H1: forall y, isVar (sigma y) /\ sigma y <> var x).
Hypothesis (N: normal s).
Hypothesis (EQ: S .+ sigma • s ≡ (var x) t).
Lemma end_is_var:
(forall x, x ∈ S -> isVar x) -> exists i e, i < |S| /\ s = var i e.
Proof.
intros H2; edestruct end_head_var as (h' & T & s' & H5 & ?); eauto. subst s.
destruct T as [| t1 [| t2 T]].
all: cbn in EQ; specialize (H1 h').
all: destruct (sigma h') eqn: H'; cbn in *; intuition.
1, 3: eapply nth_error_In in H as H7; eapply H2 in H7.
1, 2: eapply nth_error_sapp in H; rewrite ?H in EQ.
+ destruct s'; cbn in *; intuition. Discriminate.
+ rewrite AppR_subst in EQ; cbn in EQ.
eapply equiv_app_elim in EQ as (EQ1 & EQ2); cbn; eauto; simplify.
destruct s'; cbn in *; intuition.
rewrite H in EQ1. 2: rewrite H; eauto.
exfalso. symmetry in EQ1.
eapply equiv_neq_var_app; eauto; simplify; eauto.
+ exists h'. exists t1. intuition. eauto using nth_error_Some_lt.
Qed.
End BackwardDirection.
Lemma MU_PCP S':
NOU 3 (PCP_to_U S') -> PCP S'.
Proof.
intros (Delta & sigma & T & H & N); cbn in *.
repeat apply equiv_lam_elim in H.
eapply equiv_app_elim in H as [EQ2 EQ1]; cbn; intuition.
eapply equiv_app_elim in EQ2 as [_ EQ2]; cbn; intuition.
rewrite !AppR_subst in EQ1; rewrite !AppR_subst in EQ2.
rewrite !Enc_subst_id in EQ2;try reflexivity.
cbn in *. unfold funcomp in *.
rewrite !ren_plus_base, !ren_plus_combine in *;
change (1 + 1 + 1) with 3 in *.
unfold shift, var_zero in *.
rewrite map_id_list in EQ1; [| intros ? ? % repeated_in; now subst ].
assert (Delta ⊢(3) sigma 0 : Arr (repeat (alpha → alpha) (length S')) alpha) as T1
by now apply T.
specialize (N 0) as N2; eapply normal_nf in N2 as N3.
destruct N3 as [k x t' T' Hi H ->].
eapply Lambda_ordertyping_inv in T1 as (L & B & H0 & H1 & <-).
eapply id in H0 as T2.
assert (|L | <= |S'|) as L1 by
(eapply (f_equal arity) in H1; simplify in H1; rewrite H1; eauto).
symmetry in H1; eapply Arr_inversion in H1 as (L2 & H1 & H2); simplify; try omega.
eapply repeated_app_inv in H1 as (H1 & H3 & H4); eauto.
rewrite H4 in H2; subst B.
rewrite H3 in *; simplify in *. clear H3 H4 L1. revert H0 H1 EQ1 EQ2 T2 N2.
generalize (length L); generalize (length L2); clear L L2. intros l k H0 H1 EQ1 EQ2 T2 N2.
edestruct (@list_decompose_alt k _ S') as (S1 & S2 & H4 & H5); try omega; subst S'.
rewrite !Lambda_ren in EQ1; rewrite !Lambda_ren in EQ2.
simplify in EQ1 EQ2; rewrite !AppR_app in EQ1; rewrite !AppR_app in EQ2.
simplify in H1; assert (length S1 = l) as H2 by omega; clear H1; subst.
rewrite !AppR_Lambda' in EQ1, EQ2; simplify; eauto.
rewrite AppR_Lambda' in EQ2; simplify; eauto.
rewrite it_up_var_sapp in EQ1; simplify; intros; try omega.
rewrite !it_up_var_sapp in EQ2; simplify; intros; try omega.
destruct (@AppL_largest _ (fun s => match s with var x => x < |S2| | _ => False end) (AppR x T'))
as (S & t & H1 & H2 & H3). intros []; intuition; now right.
assert (exists I, I ⊆ nats (|S2|) /\ S = map var I) as [I []].
- clear H2. induction S. exists nil; cbn; intuition.
edestruct IHS as [I]; [firstorder|]. intuition; subst.
specialize (H1 a); mp H1; [firstorder|].
destruct a as [i| | |]; intuition. exists (i :: I); cbn.
eapply lt_nats in H1. intuition.
- clear H1. rewrite H2 in EQ1, EQ2.
destruct S1.
+ rewrite H2 in *. assert (normal t) by now eapply normal_AppL_right, normal_Lambda.
rewrite !AppL_subst in EQ1; rewrite !AppL_subst in EQ2. subst S. cbn -[add] in *.
rewrite !select_variables_subst in EQ2.
rewrite !select_variables_subst in EQ1.
all: simplify; eauto.
rewrite <-!select_map, !enc_concat in EQ2.
eapply AppL_ordertyping_inv in T2 as (L' & B & H8 & H9).
eapply enc_eq in EQ2; eauto.
2 - 5: intros ? EQ3;
eapply end_is_var_typed in EQ3 as (? & ? & ? & ?); cbn; simplify.
(* close False goals *)
2, 7, 12, 17: eapply H3; cbn; eauto; cbn; now simplify in *.
(* close normal term goals *)
3, 7, 11, 15: eauto.
(* close Enc goals *)
3, 6, 9, 12: reflexivity.
(* close typing goals *)
3, 5, 7, 9: eauto.
(* close var goals *)
2 - 5: intros; cbn; unfold funcomp, u, v; intuition discriminate.
exists I; intuition; eauto using nats_lt.
subst; cbn [map select concat AppL] in EQ2, EQ1.
eapply end_is_var in EQ1 as (? & ? & ? & ?);
eauto; simplify.
eapply H3; cbn; eauto; cbn; now simplify in *.
intros; cbn; intuition; discriminate.
intros ? ? % repeated_in; subst; eauto.
now rewrite !select_map in EQ2.
+ eapply id in T2 as T3.
eapply AppR_ordertyping_inv in T2 as (L' & T2 & T4).
destruct x as [i | | |]; cbn in H; eauto.
* inv T4.
assert (i < length S2 \/ i >= length S2) as [H42|H42] by omega.
** rewrite nth_error_app1, nth_error_repeated in H7; simplify; eauto.
injection H7 as H7. eapply (f_equal ord) in H7. simplify in H7.
symmetry in H7; eapply Nat.eq_le_incl in H7; simplify in H7.
intuition. cbn in H7. omega.
** rewrite <-H2 in EQ1. asimpl in EQ1. rewrite sapp_ge_in in EQ1; simplify; eauto.
eapply equiv_head_equal in EQ1; simplify; cbn; eauto.
simplify in EQ1; cbn in EQ1. discriminate EQ1.
* rewrite <-H2 in EQ1. exfalso. asimpl in EQ1.
eapply equiv_head_equal in EQ1; cbn; simplify; cbn; intuition.
cbn in EQ1; simplify in EQ1; discriminate.
Qed.
Theorem PCP_U3: PCP ⪯ OU 3 X.
Proof.
exists PCP_to_U. intros C; split; eauto using PCP_MU.
rewrite OU_NOU; eauto using MU_PCP.
Qed.
End HuetReduction.
NOU 3 (PCP_to_U S') -> PCP S'.
Proof.
intros (Delta & sigma & T & H & N); cbn in *.
repeat apply equiv_lam_elim in H.
eapply equiv_app_elim in H as [EQ2 EQ1]; cbn; intuition.
eapply equiv_app_elim in EQ2 as [_ EQ2]; cbn; intuition.
rewrite !AppR_subst in EQ1; rewrite !AppR_subst in EQ2.
rewrite !Enc_subst_id in EQ2;try reflexivity.
cbn in *. unfold funcomp in *.
rewrite !ren_plus_base, !ren_plus_combine in *;
change (1 + 1 + 1) with 3 in *.
unfold shift, var_zero in *.
rewrite map_id_list in EQ1; [| intros ? ? % repeated_in; now subst ].
assert (Delta ⊢(3) sigma 0 : Arr (repeat (alpha → alpha) (length S')) alpha) as T1
by now apply T.
specialize (N 0) as N2; eapply normal_nf in N2 as N3.
destruct N3 as [k x t' T' Hi H ->].
eapply Lambda_ordertyping_inv in T1 as (L & B & H0 & H1 & <-).
eapply id in H0 as T2.
assert (|L | <= |S'|) as L1 by
(eapply (f_equal arity) in H1; simplify in H1; rewrite H1; eauto).
symmetry in H1; eapply Arr_inversion in H1 as (L2 & H1 & H2); simplify; try omega.
eapply repeated_app_inv in H1 as (H1 & H3 & H4); eauto.
rewrite H4 in H2; subst B.
rewrite H3 in *; simplify in *. clear H3 H4 L1. revert H0 H1 EQ1 EQ2 T2 N2.
generalize (length L); generalize (length L2); clear L L2. intros l k H0 H1 EQ1 EQ2 T2 N2.
edestruct (@list_decompose_alt k _ S') as (S1 & S2 & H4 & H5); try omega; subst S'.
rewrite !Lambda_ren in EQ1; rewrite !Lambda_ren in EQ2.
simplify in EQ1 EQ2; rewrite !AppR_app in EQ1; rewrite !AppR_app in EQ2.
simplify in H1; assert (length S1 = l) as H2 by omega; clear H1; subst.
rewrite !AppR_Lambda' in EQ1, EQ2; simplify; eauto.
rewrite AppR_Lambda' in EQ2; simplify; eauto.
rewrite it_up_var_sapp in EQ1; simplify; intros; try omega.
rewrite !it_up_var_sapp in EQ2; simplify; intros; try omega.
destruct (@AppL_largest _ (fun s => match s with var x => x < |S2| | _ => False end) (AppR x T'))
as (S & t & H1 & H2 & H3). intros []; intuition; now right.
assert (exists I, I ⊆ nats (|S2|) /\ S = map var I) as [I []].
- clear H2. induction S. exists nil; cbn; intuition.
edestruct IHS as [I]; [firstorder|]. intuition; subst.
specialize (H1 a); mp H1; [firstorder|].
destruct a as [i| | |]; intuition. exists (i :: I); cbn.
eapply lt_nats in H1. intuition.
- clear H1. rewrite H2 in EQ1, EQ2.
destruct S1.
+ rewrite H2 in *. assert (normal t) by now eapply normal_AppL_right, normal_Lambda.
rewrite !AppL_subst in EQ1; rewrite !AppL_subst in EQ2. subst S. cbn -[add] in *.
rewrite !select_variables_subst in EQ2.
rewrite !select_variables_subst in EQ1.
all: simplify; eauto.
rewrite <-!select_map, !enc_concat in EQ2.
eapply AppL_ordertyping_inv in T2 as (L' & B & H8 & H9).
eapply enc_eq in EQ2; eauto.
2 - 5: intros ? EQ3;
eapply end_is_var_typed in EQ3 as (? & ? & ? & ?); cbn; simplify.
(* close False goals *)
2, 7, 12, 17: eapply H3; cbn; eauto; cbn; now simplify in *.
(* close normal term goals *)
3, 7, 11, 15: eauto.
(* close Enc goals *)
3, 6, 9, 12: reflexivity.
(* close typing goals *)
3, 5, 7, 9: eauto.
(* close var goals *)
2 - 5: intros; cbn; unfold funcomp, u, v; intuition discriminate.
exists I; intuition; eauto using nats_lt.
subst; cbn [map select concat AppL] in EQ2, EQ1.
eapply end_is_var in EQ1 as (? & ? & ? & ?);
eauto; simplify.
eapply H3; cbn; eauto; cbn; now simplify in *.
intros; cbn; intuition; discriminate.
intros ? ? % repeated_in; subst; eauto.
now rewrite !select_map in EQ2.
+ eapply id in T2 as T3.
eapply AppR_ordertyping_inv in T2 as (L' & T2 & T4).
destruct x as [i | | |]; cbn in H; eauto.
* inv T4.
assert (i < length S2 \/ i >= length S2) as [H42|H42] by omega.
** rewrite nth_error_app1, nth_error_repeated in H7; simplify; eauto.
injection H7 as H7. eapply (f_equal ord) in H7. simplify in H7.
symmetry in H7; eapply Nat.eq_le_incl in H7; simplify in H7.
intuition. cbn in H7. omega.
** rewrite <-H2 in EQ1. asimpl in EQ1. rewrite sapp_ge_in in EQ1; simplify; eauto.
eapply equiv_head_equal in EQ1; simplify; cbn; eauto.
simplify in EQ1; cbn in EQ1. discriminate EQ1.
* rewrite <-H2 in EQ1. exfalso. asimpl in EQ1.
eapply equiv_head_equal in EQ1; cbn; simplify; cbn; intuition.
cbn in EQ1; simplify in EQ1; discriminate.
Qed.
Theorem PCP_U3: PCP ⪯ OU 3 X.
Proof.
exists PCP_to_U. intros C; split; eauto using PCP_MU.
rewrite OU_NOU; eauto using MU_PCP.
Qed.
End HuetReduction.