LogRel.Checkers.Views: properties of the view-building functions.
From Coq Require Import Nat Lia.
From Equations Require Import Equations.
From PartialFun Require Import Monad PartialFun MonadExn.
From LogRel Require Import Utils BasicAst AutoSubst.Extra Context NormalForms Notations PropertiesDefinition DeclarativeTyping.
From LogRel.Checkers Require Import Functions.
Import MonadNotations.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Set Printing Universes.
Import DeclarativeTypingData.
Lemma zip_can t s : ~ isCanonical (zip1 t s).
Proof.
destruct s ; cbn.
all: now intros c ; inversion c.
Qed.
Definition dest_entry_rename (ρ : nat -> nat) (d : dest_entry) : dest_entry :=
match d with
| eEmptyElim P => eEmptyElim P⟨upRen_term_term ρ⟩
| eNatElim P hs hz => eNatElim P⟨upRen_term_term ρ⟩ hs⟨ρ⟩ hz⟨ρ⟩
| eApp u => eApp u⟨ρ⟩
| eFst => eFst
| eSnd => eSnd
| eIdElim A x P hr y => eIdElim A⟨ρ⟩ x⟨ρ⟩ P⟨upRen_term_term (upRen_term_term ρ)⟩ hr⟨ρ⟩ y⟨ρ⟩
end.
Lemma zip_rename ρ t π : (zip t π)⟨ρ⟩ = zip t⟨ρ⟩ (list_map (dest_entry_rename ρ) π).
Proof.
induction π as [|[]] in t |- * ; cbn.
1: reflexivity.
all: now erewrite IHπ.
Qed.
Lemma isType_tm_view1 t e :
build_tm_view1 t = tm_view1_type e ->
isType t × ~ whne t.
Proof.
intros H.
destruct e ; cbn.
all: split ; [ now econstructor | intros H' ; inversion H'].
Qed.
Lemma whnf_tm_view1_nat t e :
build_tm_view1 t = tm_view1_nat e ->
whnf t × ~ whne t.
Proof.
intros H.
destruct e ; cbn.
all: split ; [ now econstructor | intros H' ; inversion H'].
Qed.
Lemma build_ty_view1_anomaly t :
build_ty_view1 t = ty_view1_anomaly ->
~ isType t × isCanonical t.
Proof.
intros.
destruct t ; cbn in * ; try solve [congruence].
all: split ; [..|now constructor] ; intros H' ; inversion H' ;
eapply can_whne_exclusive ; [..|eassumption] ; constructor.
Qed.
Lemma ty_view1_small_can T n : build_ty_view1 T = ty_view1_small n -> ~ isCanonical T.
Proof.
destruct T ; cbn.
all: inversion 1.
all: inversion 1.
Qed.
Lemma tm_view1_neutral_can t n : build_nf_view1 t = nf_view1_ne n -> ~ isCanonical t.
Proof.
destruct t ; cbn.
all: inversion 1.
all: inversion 1.
Qed.
Lemma ty_view2_neutral_can T V : build_nf_ty_view2 T V = ty_neutrals T V -> ~ isCanonical T × ~ isCanonical V.
Proof.
destruct T, V ; cbn.
all: inversion 1.
all: split ; inversion 1.
Qed.
Lemma whnf_view3_ty_neutral_can s t u : build_nf_view3 (tSort s) t u = types s (ty_neutrals t u) -> ~ isCanonical t × ~ isCanonical u.
Proof.
destruct t, u ; cbn.
all: inversion 1.
all: split ; inversion 1.
Qed.
Lemma whnf_view3_neutrals_can A t u :
whnf A ->
build_nf_view3 A t u = neutrals A t u ->
[× isPosType A, ~ isCanonical t & ~ isCanonical u].
Proof.
intros HA.
simp build_nf_view3.
destruct (build_ty_view1 A) eqn:EA ; cbn.
all: try solve [inversion 1].
1: match goal with | |- context [match ?t with | _ => _ end] => destruct t eqn:? ; cbn end ;
try solve [inversion 1].
all: simp build_nf_view3 ; cbn.
all: destruct (build_nf_view1 t) eqn:? ; cbn.
all: try solve [inversion 1].
all: repeat (
match goal with | |- context [match ?t with | _ => _ end] => destruct t eqn:? ; cbn end ;
try solve [inversion 1]).
all: intros _.
all: split ; try solve [now eapply tm_view1_neutral_can].
all: econstructor.
eapply ty_view1_small_can in EA.
destruct HA ; try easy.
all: exfalso ; apply EA ; now constructor.
Qed.
Definition whne_ne_view1 {N} (w : whne N) : ne_view1 N :=
match w with
| whne_tRel => ne_view1_rel _
| whne_tApp _ => ne_view1_dest _ (eApp _)
| whne_tNatElim _ => ne_view1_dest _ (eNatElim _ _ _)
| whne_tEmptyElim _ => ne_view1_dest _ (eEmptyElim _)
| whne_tFst _ => ne_view1_dest _ eFst
| whne_tSnd _ => ne_view1_dest _ eSnd
| whne_tIdElim _ => ne_view1_dest _ (eIdElim _ _ _ _ _)
end.
Lemma whne_ty_view1 {N} (w : whne N) : build_ty_view1 N = ty_view1_small (whne_ne_view1 w).
Proof.
now destruct w.
Qed.
Lemma whne_nf_view1 {N} (w : whne N) : build_nf_view1 N = nf_view1_ne (whne_ne_view1 w).
Proof.
now destruct w.
Qed.
Lemma whne_ty_view2 {M N} (wM : whne M) (wN : whne N) : build_nf_ty_view2 M N = ty_neutrals M N.
Proof.
simp build_nf_ty_view2.
unshelve erewrite ! whne_ty_view1 ; tea.
now reflexivity.
Qed.
Lemma whne_nf_view3 P m n (wP : isPosType P) (wm : whne m) (wn : whne n) :
build_nf_view3 P m n =
(match wP with
| UnivPos => types _ (ty_neutrals m n)
| _ => neutrals _ m n
end).
Proof.
simp build_nf_view3.
destruct wP ; cbn.
2-4: unshelve erewrite whne_nf_view1 ; tea; cbn; now rewrite (whne_nf_view1 wn).
- rewrite whne_ty_view2 ; cbn ; tea.
reflexivity.
- unshelve erewrite whne_ty_view1 ; tea.
cbn.
unshelve erewrite whne_nf_view1 ; tea ; cbn.
destruct (build_nf_view1 _) eqn:e ; try easy.
all: unshelve erewrite whne_nf_view1 in e ; tea.
all: inversion e.
Qed.
Lemma ty_mismatch_hd_view Γ T V (tT : isType T) (tV : isType V) :
build_nf_ty_view2 T V = ty_mismatch T V ->
type_hd_view Γ tT tV = False.
Proof.
destruct tT, tV ; cbn ; try reflexivity.
all: simp build_nf_ty_view2 ; cbn.
1-6: congruence.
do 2 (unshelve erewrite whne_ty_view1 ; tea) ; cbn.
congruence.
Qed.
Lemma univ_mismatch_hd_view Γ s T V (tT : isType T) (tV : isType V) :
build_nf_view3 (tSort s) T V = types s (ty_mismatch T V) ->
univ_hd_view Γ tT tV = False.
Proof.
destruct tT, tV ; cbn ; try reflexivity.
all: simp build_nf_view3 build_nf_ty_view2 ; cbn.
1-5: intros [=].
do 2 (unshelve erewrite whne_ty_view1 ; tea) ; cbn.
discriminate.
Qed.
Lemma mismatch_hd_view Γ A t u (tA : isType A) :
whnf t -> whnf u ->
build_nf_view3 A t u = mismatch A t u ->
(∑ (nft : isNat t) (nfu : isNat u), A = tNat × nat_hd_view Γ nft nfu = False) +
(∑ (nft : isId t) (nfu : isId u) A' x y, A = tId A' x y × id_hd_view Γ A' x y nft nfu = False).
Proof.
intros wt wu.
destruct tA ; cbn.
all: simp build_nf_view3 build_nf_ty_view2 ; cbn.
all: try solve [intros [=]].
- destruct (build_nf_view1 t), (build_nf_view1 u) ; cbn.
all: try solve [intros [=]].
all: destruct n ; cbn ; try solve [intros [=]].
all: destruct n0 ; cbn ; try solve [intros [=]].
all: unshelve (intros _ ; left ; do 2 eexists).
all: try solve [constructor].
1-8: econstructor ; eapply not_can_whne ; tea ; solve [now apply zip_can | intros c ; inversion c].
all: now cbn.
- destruct (build_nf_view1 t), (build_nf_view1 u) ; cbn.
all: solve [intros [=]].
- destruct (build_nf_view1 t), (build_nf_view1 u) ; cbn.
all: try solve [intros [=]].
all: destruct n ; cbn ; try solve [intros [=]].
all: (intros _ ; right ; do 5 eexists).
all: split ; [reflexivity|..].
Unshelve.
all: try solve [constructor].
5-8: econstructor ; eapply not_can_whne ; tea ; solve [now apply zip_can | intros c ; inversion c].
all: now cbn.
- unshelve erewrite whne_ty_view1 ; tea ; cbn.
destruct (build_nf_view1 t) ; cbn ; try solve [intros [=]].
destruct (build_nf_view1 u) ; cbn ; solve [intros [=]].
Qed.
Definition ncan_ne_view1 {N} (w : ~ isCanonical N) : ne_view1 N.
Proof.
destruct N.
all: try solve [destruct w ; econstructor].
- now constructor.
- eapply (ne_view1_dest _ (eApp _)).
- eapply (ne_view1_dest _ (eNatElim _ _ _)).
- eapply (ne_view1_dest _ (eEmptyElim _)).
- eapply (ne_view1_dest _ eFst).
- eapply (ne_view1_dest _ eSnd).
- eapply (ne_view1_dest _ (eIdElim _ _ _ _ _)).
Defined.
Lemma ncan_nf_view1 {N} (w : ~ isCanonical N) :
build_nf_view1 N = nf_view1_ne (ncan_ne_view1 w).
Proof.
destruct N ; cbn ; try reflexivity.
all: destruct w ; econstructor.
Qed.
Lemma nf_view2_neutral_can t t' :
build_nf_view2 t t' = neutrals2 t t' ->
~ isCanonical t /\ ~ isCanonical t'.
Proof.
intros Heq.
simp build_nf_view2 in Heq.
destruct (build_nf_view1 t) as [? [] | | ? [] | | | ] eqn:Heqt ; cbn in Heq.
all: destruct (build_nf_view1 t') as [? [] | | ? [] | | | ] eqn:Heqt' ; cbn in Heq.
all: try solve [congruence].
split.
all: now eapply tm_view1_neutral_can.
Qed.
Lemma mismatch2_hd_view_ty Γ T V (tT : isType T) (tV : isType V) :
build_nf_view2 T V = mismatch2 T V ->
type_hd_view Γ tT tV = False.
Proof.
destruct tT, tV ; cbn ; try reflexivity.
all: simp build_nf_view2 ; cbn.
1-6: congruence.
do 2 (unshelve erewrite whne_nf_view1 ; tea ; cbn).
congruence.
Qed.
Lemma mismatch2_hd_view_tm Γ A t u :
[Γ |-[de] t : A] -> [Γ |-[de] u : A] ->
whnf t -> whnf u ->
build_nf_view2 t u = mismatch2 t u ->
(∑ (nft : isType t) (nfu : isType u), type_hd_view Γ nft nfu = False) +
((∑ (nft : isNat t) (nfu : isNat u), nat_hd_view Γ nft nfu = False) +
(∑ (nft : isId t) (nfu : isId u) , forall Γ A' x y, id_hd_view Γ A' x y nft nfu = False)).
Proof.
intros Ht Hu wt wu.
funelim (build_nf_view2 t u).
all: try solve [
congruence |
match goal with
| H : [_ |-[de] (tSort _) : _] |- _ => eapply termGen' in H as (?&[]&?)
end |
left ; unshelve (do 2 eexists) ; try constructor ; cbn ;
now apply not_can_whne ; [..|eapply tm_view1_neutral_can] |
right ; left ; unshelve (do 2 eexists) ; try constructor ; cbn ;
now apply not_can_whne ; [..|eapply tm_view1_neutral_can]].
1,4: unshelve (right ; right ; unshelve (do 2 eexists) ; econstructor ;
[now apply not_can_whne ; [..|eapply tm_view1_neutral_can]|..] ;
do 2 eexists ; reflexivity) ; easy.
- destruct t1 ; try solve [congruence |
left ; unshelve (do 2 eexists) ; try constructor ; cbn ;
now apply not_can_whne ; [..|eapply tm_view1_neutral_can]].
- destruct n ;
try solve [
congruence |
right ; left ; unshelve (do 2 eexists) ; try constructor ; cbn ;
now apply not_can_whne ; [..|eapply tm_view1_neutral_can]].
Qed.
Lemma mismatch2_hd_view_ne t u :
whne t -> whne u ->
~ build_nf_view2 t u = mismatch2 t u.
Proof.
intros Ht Hu.
funelim (build_nf_view2 _ _) ; try solve [congruence|inversion Hu|inversion Ht].
- destruct t1 ; inversion Hu.
- destruct n ; inversion Hu.
Qed.
Definition nf_view2_rename (ρ : nat -> nat) {t t' : term} (v : nf_view2 t t') : nf_view2 t⟨ρ⟩ t'⟨ρ⟩ :=
match v in nf_view2 x x' return nf_view2 x⟨ρ⟩ x'⟨ρ⟩ with
| sorts2 s s' => sorts2 s s'
| prods2 A A' B B' => prods2 A⟨ρ⟩ A'⟨ρ⟩ B⟨upRen_term_term ρ⟩ B'⟨upRen_term_term ρ⟩
| nats2 => nats2
| emptys2 => emptys2
| sigs2 A A' B B' => sigs2 A⟨ρ⟩ A'⟨ρ⟩ B⟨upRen_term_term ρ⟩ B'⟨upRen_term_term ρ⟩
| ids2 A A' x x' y y' => ids2 A⟨ρ⟩ A'⟨ρ⟩ x⟨ρ⟩ x'⟨ρ⟩ y⟨ρ⟩ y'⟨ρ⟩
| lams2 A A' t t' => lams2 A⟨ρ⟩ A'⟨ρ⟩ t⟨upRen_term_term ρ⟩ t'⟨upRen_term_term ρ⟩
| lam_ne2 A t n' => lam_ne2 A⟨ρ⟩ t⟨upRen_term_term ρ⟩ n'⟨ρ⟩
| ne_lam2 n A' t' => ne_lam2 n⟨ρ⟩ A'⟨ρ⟩ t'⟨upRen_term_term ρ⟩
| zeros2 => zeros2
| succs2 t t' => succs2 t⟨ρ⟩ t'⟨ρ⟩
| pairs2 A A' B B' t t' u u' =>
pairs2 A⟨ρ⟩ A'⟨ρ⟩ B⟨upRen_term_term ρ⟩ B'⟨upRen_term_term ρ⟩ t⟨ρ⟩ t'⟨ρ⟩ u⟨ρ⟩ u'⟨ρ⟩
| pair_ne2 A B t u n' => pair_ne2 A⟨ρ⟩ B⟨upRen_term_term ρ⟩ t⟨ρ⟩ u⟨ρ⟩ n'⟨ρ⟩
| ne_pair2 n A' B' t' u' => ne_pair2 n⟨ρ⟩ A'⟨ρ⟩ B'⟨upRen_term_term ρ⟩ t'⟨ρ⟩ u'⟨ρ⟩
| refls2 A A' x x' => refls2 A⟨ρ⟩ A'⟨ρ⟩ x⟨ρ⟩ x'⟨ρ⟩
| neutrals2 n n' => neutrals2 n⟨ρ⟩ n'⟨ρ⟩
| mismatch2 t u => mismatch2 t⟨ρ⟩ u⟨ρ⟩
| anomaly2 t u => anomaly2 t⟨ρ⟩ u⟨ρ⟩
end.
Lemma build_nf_view2_rename ρ t t' : build_nf_view2 t⟨ρ⟩ t'⟨ρ⟩ = nf_view2_rename ρ (build_nf_view2 t t').
Proof.
destruct t, t' ; reflexivity.
Qed.
Definition ne_view2_rename (ρ : nat -> nat) {t t' : term} (v : ne_view2 t t') : ne_view2 t⟨ρ⟩ t'⟨ρ⟩ :=
match v in ne_view2 x x' return ne_view2 x⟨ρ⟩ x'⟨ρ⟩ with
| ne_rels n n' => ne_rels (ρ n) (ρ n')
| ne_apps f u f' u' => ne_apps f⟨ρ⟩ u⟨ρ⟩ f'⟨ρ⟩ u'⟨ρ⟩
| ne_nats n P hz hs n' P' hz' hs' => ne_nats
n⟨ρ⟩ P⟨upRen_term_term ρ⟩ hz⟨ρ⟩ hs⟨ρ⟩
n'⟨ρ⟩ P'⟨upRen_term_term ρ⟩ hz'⟨ρ⟩ hs'⟨ρ⟩
| ne_emptys n P n' P' => ne_emptys n⟨ρ⟩ P⟨upRen_term_term ρ⟩ n'⟨ρ⟩ P'⟨upRen_term_term ρ⟩
| ne_fsts p p' => ne_fsts p⟨ρ⟩ p'⟨ρ⟩
| ne_snds p p' => ne_snds p⟨ρ⟩ p'⟨ρ⟩
| ne_ids A x P hr y e A' x' P' hr' y' e' => ne_ids
A⟨ρ⟩ x⟨ρ⟩ P⟨upRen_term_term (upRen_term_term ρ)⟩ hr⟨ρ⟩ y⟨ρ⟩ e⟨ρ⟩
A'⟨ρ⟩ x'⟨ρ⟩ P'⟨upRen_term_term (upRen_term_term ρ)⟩ hr'⟨ρ⟩ y'⟨ρ⟩ e'⟨ρ⟩
| ne_mismatch t u => ne_mismatch t⟨ρ⟩ u⟨ρ⟩
| ne_anomaly t u => ne_anomaly t⟨ρ⟩ u⟨ρ⟩
end.
Lemma build_ne_view2_rename ρ t t' : build_ne_view2 t⟨ρ⟩ t'⟨ρ⟩ = ne_view2_rename ρ (build_ne_view2 t t').
Proof.
destruct t, t' ; reflexivity.
Qed.
From Equations Require Import Equations.
From PartialFun Require Import Monad PartialFun MonadExn.
From LogRel Require Import Utils BasicAst AutoSubst.Extra Context NormalForms Notations PropertiesDefinition DeclarativeTyping.
From LogRel.Checkers Require Import Functions.
Import MonadNotations.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Set Printing Universes.
Import DeclarativeTypingData.
Lemma zip_can t s : ~ isCanonical (zip1 t s).
Proof.
destruct s ; cbn.
all: now intros c ; inversion c.
Qed.
Definition dest_entry_rename (ρ : nat -> nat) (d : dest_entry) : dest_entry :=
match d with
| eEmptyElim P => eEmptyElim P⟨upRen_term_term ρ⟩
| eNatElim P hs hz => eNatElim P⟨upRen_term_term ρ⟩ hs⟨ρ⟩ hz⟨ρ⟩
| eApp u => eApp u⟨ρ⟩
| eFst => eFst
| eSnd => eSnd
| eIdElim A x P hr y => eIdElim A⟨ρ⟩ x⟨ρ⟩ P⟨upRen_term_term (upRen_term_term ρ)⟩ hr⟨ρ⟩ y⟨ρ⟩
end.
Lemma zip_rename ρ t π : (zip t π)⟨ρ⟩ = zip t⟨ρ⟩ (list_map (dest_entry_rename ρ) π).
Proof.
induction π as [|[]] in t |- * ; cbn.
1: reflexivity.
all: now erewrite IHπ.
Qed.
Lemma isType_tm_view1 t e :
build_tm_view1 t = tm_view1_type e ->
isType t × ~ whne t.
Proof.
intros H.
destruct e ; cbn.
all: split ; [ now econstructor | intros H' ; inversion H'].
Qed.
Lemma whnf_tm_view1_nat t e :
build_tm_view1 t = tm_view1_nat e ->
whnf t × ~ whne t.
Proof.
intros H.
destruct e ; cbn.
all: split ; [ now econstructor | intros H' ; inversion H'].
Qed.
Lemma build_ty_view1_anomaly t :
build_ty_view1 t = ty_view1_anomaly ->
~ isType t × isCanonical t.
Proof.
intros.
destruct t ; cbn in * ; try solve [congruence].
all: split ; [..|now constructor] ; intros H' ; inversion H' ;
eapply can_whne_exclusive ; [..|eassumption] ; constructor.
Qed.
Lemma ty_view1_small_can T n : build_ty_view1 T = ty_view1_small n -> ~ isCanonical T.
Proof.
destruct T ; cbn.
all: inversion 1.
all: inversion 1.
Qed.
Lemma tm_view1_neutral_can t n : build_nf_view1 t = nf_view1_ne n -> ~ isCanonical t.
Proof.
destruct t ; cbn.
all: inversion 1.
all: inversion 1.
Qed.
Lemma ty_view2_neutral_can T V : build_nf_ty_view2 T V = ty_neutrals T V -> ~ isCanonical T × ~ isCanonical V.
Proof.
destruct T, V ; cbn.
all: inversion 1.
all: split ; inversion 1.
Qed.
Lemma whnf_view3_ty_neutral_can s t u : build_nf_view3 (tSort s) t u = types s (ty_neutrals t u) -> ~ isCanonical t × ~ isCanonical u.
Proof.
destruct t, u ; cbn.
all: inversion 1.
all: split ; inversion 1.
Qed.
Lemma whnf_view3_neutrals_can A t u :
whnf A ->
build_nf_view3 A t u = neutrals A t u ->
[× isPosType A, ~ isCanonical t & ~ isCanonical u].
Proof.
intros HA.
simp build_nf_view3.
destruct (build_ty_view1 A) eqn:EA ; cbn.
all: try solve [inversion 1].
1: match goal with | |- context [match ?t with | _ => _ end] => destruct t eqn:? ; cbn end ;
try solve [inversion 1].
all: simp build_nf_view3 ; cbn.
all: destruct (build_nf_view1 t) eqn:? ; cbn.
all: try solve [inversion 1].
all: repeat (
match goal with | |- context [match ?t with | _ => _ end] => destruct t eqn:? ; cbn end ;
try solve [inversion 1]).
all: intros _.
all: split ; try solve [now eapply tm_view1_neutral_can].
all: econstructor.
eapply ty_view1_small_can in EA.
destruct HA ; try easy.
all: exfalso ; apply EA ; now constructor.
Qed.
Definition whne_ne_view1 {N} (w : whne N) : ne_view1 N :=
match w with
| whne_tRel => ne_view1_rel _
| whne_tApp _ => ne_view1_dest _ (eApp _)
| whne_tNatElim _ => ne_view1_dest _ (eNatElim _ _ _)
| whne_tEmptyElim _ => ne_view1_dest _ (eEmptyElim _)
| whne_tFst _ => ne_view1_dest _ eFst
| whne_tSnd _ => ne_view1_dest _ eSnd
| whne_tIdElim _ => ne_view1_dest _ (eIdElim _ _ _ _ _)
end.
Lemma whne_ty_view1 {N} (w : whne N) : build_ty_view1 N = ty_view1_small (whne_ne_view1 w).
Proof.
now destruct w.
Qed.
Lemma whne_nf_view1 {N} (w : whne N) : build_nf_view1 N = nf_view1_ne (whne_ne_view1 w).
Proof.
now destruct w.
Qed.
Lemma whne_ty_view2 {M N} (wM : whne M) (wN : whne N) : build_nf_ty_view2 M N = ty_neutrals M N.
Proof.
simp build_nf_ty_view2.
unshelve erewrite ! whne_ty_view1 ; tea.
now reflexivity.
Qed.
Lemma whne_nf_view3 P m n (wP : isPosType P) (wm : whne m) (wn : whne n) :
build_nf_view3 P m n =
(match wP with
| UnivPos => types _ (ty_neutrals m n)
| _ => neutrals _ m n
end).
Proof.
simp build_nf_view3.
destruct wP ; cbn.
2-4: unshelve erewrite whne_nf_view1 ; tea; cbn; now rewrite (whne_nf_view1 wn).
- rewrite whne_ty_view2 ; cbn ; tea.
reflexivity.
- unshelve erewrite whne_ty_view1 ; tea.
cbn.
unshelve erewrite whne_nf_view1 ; tea ; cbn.
destruct (build_nf_view1 _) eqn:e ; try easy.
all: unshelve erewrite whne_nf_view1 in e ; tea.
all: inversion e.
Qed.
Lemma ty_mismatch_hd_view Γ T V (tT : isType T) (tV : isType V) :
build_nf_ty_view2 T V = ty_mismatch T V ->
type_hd_view Γ tT tV = False.
Proof.
destruct tT, tV ; cbn ; try reflexivity.
all: simp build_nf_ty_view2 ; cbn.
1-6: congruence.
do 2 (unshelve erewrite whne_ty_view1 ; tea) ; cbn.
congruence.
Qed.
Lemma univ_mismatch_hd_view Γ s T V (tT : isType T) (tV : isType V) :
build_nf_view3 (tSort s) T V = types s (ty_mismatch T V) ->
univ_hd_view Γ tT tV = False.
Proof.
destruct tT, tV ; cbn ; try reflexivity.
all: simp build_nf_view3 build_nf_ty_view2 ; cbn.
1-5: intros [=].
do 2 (unshelve erewrite whne_ty_view1 ; tea) ; cbn.
discriminate.
Qed.
Lemma mismatch_hd_view Γ A t u (tA : isType A) :
whnf t -> whnf u ->
build_nf_view3 A t u = mismatch A t u ->
(∑ (nft : isNat t) (nfu : isNat u), A = tNat × nat_hd_view Γ nft nfu = False) +
(∑ (nft : isId t) (nfu : isId u) A' x y, A = tId A' x y × id_hd_view Γ A' x y nft nfu = False).
Proof.
intros wt wu.
destruct tA ; cbn.
all: simp build_nf_view3 build_nf_ty_view2 ; cbn.
all: try solve [intros [=]].
- destruct (build_nf_view1 t), (build_nf_view1 u) ; cbn.
all: try solve [intros [=]].
all: destruct n ; cbn ; try solve [intros [=]].
all: destruct n0 ; cbn ; try solve [intros [=]].
all: unshelve (intros _ ; left ; do 2 eexists).
all: try solve [constructor].
1-8: econstructor ; eapply not_can_whne ; tea ; solve [now apply zip_can | intros c ; inversion c].
all: now cbn.
- destruct (build_nf_view1 t), (build_nf_view1 u) ; cbn.
all: solve [intros [=]].
- destruct (build_nf_view1 t), (build_nf_view1 u) ; cbn.
all: try solve [intros [=]].
all: destruct n ; cbn ; try solve [intros [=]].
all: (intros _ ; right ; do 5 eexists).
all: split ; [reflexivity|..].
Unshelve.
all: try solve [constructor].
5-8: econstructor ; eapply not_can_whne ; tea ; solve [now apply zip_can | intros c ; inversion c].
all: now cbn.
- unshelve erewrite whne_ty_view1 ; tea ; cbn.
destruct (build_nf_view1 t) ; cbn ; try solve [intros [=]].
destruct (build_nf_view1 u) ; cbn ; solve [intros [=]].
Qed.
Definition ncan_ne_view1 {N} (w : ~ isCanonical N) : ne_view1 N.
Proof.
destruct N.
all: try solve [destruct w ; econstructor].
- now constructor.
- eapply (ne_view1_dest _ (eApp _)).
- eapply (ne_view1_dest _ (eNatElim _ _ _)).
- eapply (ne_view1_dest _ (eEmptyElim _)).
- eapply (ne_view1_dest _ eFst).
- eapply (ne_view1_dest _ eSnd).
- eapply (ne_view1_dest _ (eIdElim _ _ _ _ _)).
Defined.
Lemma ncan_nf_view1 {N} (w : ~ isCanonical N) :
build_nf_view1 N = nf_view1_ne (ncan_ne_view1 w).
Proof.
destruct N ; cbn ; try reflexivity.
all: destruct w ; econstructor.
Qed.
Lemma nf_view2_neutral_can t t' :
build_nf_view2 t t' = neutrals2 t t' ->
~ isCanonical t /\ ~ isCanonical t'.
Proof.
intros Heq.
simp build_nf_view2 in Heq.
destruct (build_nf_view1 t) as [? [] | | ? [] | | | ] eqn:Heqt ; cbn in Heq.
all: destruct (build_nf_view1 t') as [? [] | | ? [] | | | ] eqn:Heqt' ; cbn in Heq.
all: try solve [congruence].
split.
all: now eapply tm_view1_neutral_can.
Qed.
Lemma mismatch2_hd_view_ty Γ T V (tT : isType T) (tV : isType V) :
build_nf_view2 T V = mismatch2 T V ->
type_hd_view Γ tT tV = False.
Proof.
destruct tT, tV ; cbn ; try reflexivity.
all: simp build_nf_view2 ; cbn.
1-6: congruence.
do 2 (unshelve erewrite whne_nf_view1 ; tea ; cbn).
congruence.
Qed.
Lemma mismatch2_hd_view_tm Γ A t u :
[Γ |-[de] t : A] -> [Γ |-[de] u : A] ->
whnf t -> whnf u ->
build_nf_view2 t u = mismatch2 t u ->
(∑ (nft : isType t) (nfu : isType u), type_hd_view Γ nft nfu = False) +
((∑ (nft : isNat t) (nfu : isNat u), nat_hd_view Γ nft nfu = False) +
(∑ (nft : isId t) (nfu : isId u) , forall Γ A' x y, id_hd_view Γ A' x y nft nfu = False)).
Proof.
intros Ht Hu wt wu.
funelim (build_nf_view2 t u).
all: try solve [
congruence |
match goal with
| H : [_ |-[de] (tSort _) : _] |- _ => eapply termGen' in H as (?&[]&?)
end |
left ; unshelve (do 2 eexists) ; try constructor ; cbn ;
now apply not_can_whne ; [..|eapply tm_view1_neutral_can] |
right ; left ; unshelve (do 2 eexists) ; try constructor ; cbn ;
now apply not_can_whne ; [..|eapply tm_view1_neutral_can]].
1,4: unshelve (right ; right ; unshelve (do 2 eexists) ; econstructor ;
[now apply not_can_whne ; [..|eapply tm_view1_neutral_can]|..] ;
do 2 eexists ; reflexivity) ; easy.
- destruct t1 ; try solve [congruence |
left ; unshelve (do 2 eexists) ; try constructor ; cbn ;
now apply not_can_whne ; [..|eapply tm_view1_neutral_can]].
- destruct n ;
try solve [
congruence |
right ; left ; unshelve (do 2 eexists) ; try constructor ; cbn ;
now apply not_can_whne ; [..|eapply tm_view1_neutral_can]].
Qed.
Lemma mismatch2_hd_view_ne t u :
whne t -> whne u ->
~ build_nf_view2 t u = mismatch2 t u.
Proof.
intros Ht Hu.
funelim (build_nf_view2 _ _) ; try solve [congruence|inversion Hu|inversion Ht].
- destruct t1 ; inversion Hu.
- destruct n ; inversion Hu.
Qed.
Definition nf_view2_rename (ρ : nat -> nat) {t t' : term} (v : nf_view2 t t') : nf_view2 t⟨ρ⟩ t'⟨ρ⟩ :=
match v in nf_view2 x x' return nf_view2 x⟨ρ⟩ x'⟨ρ⟩ with
| sorts2 s s' => sorts2 s s'
| prods2 A A' B B' => prods2 A⟨ρ⟩ A'⟨ρ⟩ B⟨upRen_term_term ρ⟩ B'⟨upRen_term_term ρ⟩
| nats2 => nats2
| emptys2 => emptys2
| sigs2 A A' B B' => sigs2 A⟨ρ⟩ A'⟨ρ⟩ B⟨upRen_term_term ρ⟩ B'⟨upRen_term_term ρ⟩
| ids2 A A' x x' y y' => ids2 A⟨ρ⟩ A'⟨ρ⟩ x⟨ρ⟩ x'⟨ρ⟩ y⟨ρ⟩ y'⟨ρ⟩
| lams2 A A' t t' => lams2 A⟨ρ⟩ A'⟨ρ⟩ t⟨upRen_term_term ρ⟩ t'⟨upRen_term_term ρ⟩
| lam_ne2 A t n' => lam_ne2 A⟨ρ⟩ t⟨upRen_term_term ρ⟩ n'⟨ρ⟩
| ne_lam2 n A' t' => ne_lam2 n⟨ρ⟩ A'⟨ρ⟩ t'⟨upRen_term_term ρ⟩
| zeros2 => zeros2
| succs2 t t' => succs2 t⟨ρ⟩ t'⟨ρ⟩
| pairs2 A A' B B' t t' u u' =>
pairs2 A⟨ρ⟩ A'⟨ρ⟩ B⟨upRen_term_term ρ⟩ B'⟨upRen_term_term ρ⟩ t⟨ρ⟩ t'⟨ρ⟩ u⟨ρ⟩ u'⟨ρ⟩
| pair_ne2 A B t u n' => pair_ne2 A⟨ρ⟩ B⟨upRen_term_term ρ⟩ t⟨ρ⟩ u⟨ρ⟩ n'⟨ρ⟩
| ne_pair2 n A' B' t' u' => ne_pair2 n⟨ρ⟩ A'⟨ρ⟩ B'⟨upRen_term_term ρ⟩ t'⟨ρ⟩ u'⟨ρ⟩
| refls2 A A' x x' => refls2 A⟨ρ⟩ A'⟨ρ⟩ x⟨ρ⟩ x'⟨ρ⟩
| neutrals2 n n' => neutrals2 n⟨ρ⟩ n'⟨ρ⟩
| mismatch2 t u => mismatch2 t⟨ρ⟩ u⟨ρ⟩
| anomaly2 t u => anomaly2 t⟨ρ⟩ u⟨ρ⟩
end.
Lemma build_nf_view2_rename ρ t t' : build_nf_view2 t⟨ρ⟩ t'⟨ρ⟩ = nf_view2_rename ρ (build_nf_view2 t t').
Proof.
destruct t, t' ; reflexivity.
Qed.
Definition ne_view2_rename (ρ : nat -> nat) {t t' : term} (v : ne_view2 t t') : ne_view2 t⟨ρ⟩ t'⟨ρ⟩ :=
match v in ne_view2 x x' return ne_view2 x⟨ρ⟩ x'⟨ρ⟩ with
| ne_rels n n' => ne_rels (ρ n) (ρ n')
| ne_apps f u f' u' => ne_apps f⟨ρ⟩ u⟨ρ⟩ f'⟨ρ⟩ u'⟨ρ⟩
| ne_nats n P hz hs n' P' hz' hs' => ne_nats
n⟨ρ⟩ P⟨upRen_term_term ρ⟩ hz⟨ρ⟩ hs⟨ρ⟩
n'⟨ρ⟩ P'⟨upRen_term_term ρ⟩ hz'⟨ρ⟩ hs'⟨ρ⟩
| ne_emptys n P n' P' => ne_emptys n⟨ρ⟩ P⟨upRen_term_term ρ⟩ n'⟨ρ⟩ P'⟨upRen_term_term ρ⟩
| ne_fsts p p' => ne_fsts p⟨ρ⟩ p'⟨ρ⟩
| ne_snds p p' => ne_snds p⟨ρ⟩ p'⟨ρ⟩
| ne_ids A x P hr y e A' x' P' hr' y' e' => ne_ids
A⟨ρ⟩ x⟨ρ⟩ P⟨upRen_term_term (upRen_term_term ρ)⟩ hr⟨ρ⟩ y⟨ρ⟩ e⟨ρ⟩
A'⟨ρ⟩ x'⟨ρ⟩ P'⟨upRen_term_term (upRen_term_term ρ)⟩ hr'⟨ρ⟩ y'⟨ρ⟩ e'⟨ρ⟩
| ne_mismatch t u => ne_mismatch t⟨ρ⟩ u⟨ρ⟩
| ne_anomaly t u => ne_anomaly t⟨ρ⟩ u⟨ρ⟩
end.
Lemma build_ne_view2_rename ρ t t' : build_ne_view2 t⟨ρ⟩ t'⟨ρ⟩ = ne_view2_rename ρ (build_ne_view2 t t').
Proof.
destruct t, t' ; reflexivity.
Qed.