Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Definition of weak-head-reduction and proof of unicity of derivations #543

Draft
wants to merge 208 commits into
base: coq-8.11
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
208 commits
Select commit Hold shift + click to select a range
8434f9f
WIP
jakobbotsch Dec 11, 2020
316f303
WIP
jakobbotsch Dec 12, 2020
94fe9bf
Updated template-coq to new case representation
mattam82 Dec 14, 2020
0abf8ec
Started updating PCUIC
mattam82 Dec 14, 2020
9c742bb
WIP in lift_subst. Needs better solve_all
mattam82 Dec 14, 2020
1657d71
Extend All_Forall with OnOne2i theory
mattam82 Dec 15, 2020
67e2469
Update typing and reduction to new branch representation. Also factor…
mattam82 Dec 15, 2020
ef2f53c
Generalize map_predicate to take a universe instance mapping function.
mattam82 Dec 16, 2020
1b73236
WP in PCUIC
mattam82 Dec 16, 2020
84c53b3
WIP in reduction
mattam82 Dec 17, 2020
f502f79
New PCUICCases file with context building predicates. Finished updati…
mattam82 Dec 19, 2020
533bef5
Improve predicate equality to take care of binder relevance annotations
mattam82 Dec 19, 2020
bae4d15
Finished (partial) PCUICNameless proof
mattam82 Dec 19, 2020
a9c5ab8
WIP in PCUICClosed
mattam82 Dec 19, 2020
50f153d
Finished PCUICClosed
mattam82 Dec 19, 2020
49909c5
In PCUICNormal. will need to rely on wf environment
mattam82 Dec 19, 2020
b1f09a6
Trying to find the right hypotheses on reduction: everything gets ugl…
mattam82 Dec 21, 2020
30c94e2
Bite the bullet and cleanup the representation of constructors of ind…
mattam82 Dec 21, 2020
a3d5866
WIP with cleaned-up inductive and constructor representation
mattam82 Dec 21, 2020
0f21b68
WIP renaming
mattam82 Dec 21, 2020
7a73d53
Done up to TypingWf
mattam82 Dec 21, 2020
e4aae53
Updated upto PCUICTyping
mattam82 Dec 21, 2020
54ed6d4
PCUICNormal working now
mattam82 Dec 21, 2020
ebc9216
Directly map on constructor list in case reduction
mattam82 Dec 21, 2020
138ca1f
Now in sigmacalculus. Need to cleanup substitution/lifting lemmas for…
mattam82 Dec 21, 2020
a9f14aa
WIP proviing renaming lemma
mattam82 Dec 22, 2020
676f1b2
Cleanup PCUICClosed to use the right unfolding behaviors
mattam82 Dec 22, 2020
c61c55c
Almost complete nameless proof
mattam82 Dec 23, 2020
be5f608
De bruijn bug in map_constructor_body...
mattam82 Dec 23, 2020
528de5b
Cleaning up sigma calculus proofs
mattam82 Dec 23, 2020
6714426
Fix replace.sh
mattam82 Dec 23, 2020
4f55189
Switched arguments of declared_inductive
mattam82 Dec 23, 2020
ff845cc
Fic declared_constructor argument order
mattam82 Dec 23, 2020
c294bd7
Change declared_projection argument order
mattam82 Dec 23, 2020
bd32ff3
Big refactoring / cleanup of sigma calculus
mattam82 Dec 23, 2020
289b8b5
SigmaCalculus is now self-contained and does not depend on Closed
mattam82 Dec 23, 2020
0a205ee
Better induction principle for "generated" contexts (fix/case/branches)
mattam82 Dec 24, 2020
fbd5584
Refactoring and proving renaming theorem
mattam82 Dec 24, 2020
d18eb24
Completed renaming proof with new case.
mattam82 Dec 24, 2020
dc507c2
Prove weakening... from instantiation
mattam82 Dec 24, 2020
f7a3612
Strenghten renaming theorem for exchange and strengthening.
mattam82 Dec 26, 2020
bc2366b
WIP finishing strengthening
mattam82 Dec 26, 2020
8a5c296
WIP on renaming proofs carrying variable information
mattam82 Dec 26, 2020
2f37033
Finished proof that reduction preserves free variables
mattam82 Dec 27, 2020
78881fd
Need to think about how to state the exchange lemma
mattam82 Dec 27, 2020
537b9d3
Proven renaming for shiftnP predicate
mattam82 Dec 27, 2020
d2df801
Play with strengthening: not provable inductively as conversions can …
mattam82 Dec 28, 2020
5dd9644
Verified proof idea for strengthening (will have to come after subjec…
mattam82 Dec 28, 2020
2a53557
Cleanup Weakening, move on_free_vars to a separate library
mattam82 Jan 4, 2021
82c7d4e
WIP in instantiation theorem
mattam82 Jan 4, 2021
eb7f0b4
Only instantiation for cumulativity remaining
mattam82 Jan 5, 2021
80c662c
Only eq_term upto instantiation remains
mattam82 Jan 5, 2021
1e119c6
Finished instantiation proof
mattam82 Jan 5, 2021
81aa326
Updating substitution and universe instantiation
mattam82 Jan 6, 2021
6f8fdd9
Before moving to overloaded subst_instance operation everywhere
mattam82 Jan 6, 2021
24e6b2c
Use overloaded subst_instance in template-coq
mattam82 Jan 6, 2021
43c13cc
Cleanup name of subst_instance lemmatas
mattam82 Jan 6, 2021
3da3351
Half of universe instantiation done
mattam82 Jan 6, 2021
9e58182
Updated univ substitution
mattam82 Jan 7, 2021
50190ca
Finished implementing substitution through instantiation. substitutio…
mattam82 Jan 7, 2021
3f6d0b8
WIP in substitution lemmas
mattam82 Jan 7, 2021
c2be5a1
Finished substitution
mattam82 Jan 8, 2021
bb61a04
Updating Parallel Reduction to carry well-formedness predicates
mattam82 Jan 8, 2021
fe9dfa2
Try a simpler solution for pred allowing reflexivity on case
mattam82 Jan 8, 2021
ec88526
WIP
mattam82 Jan 8, 2021
a891b73
Move to PCUIC having expanded contexts in Case nodes
mattam82 Jan 9, 2021
f954b2c
Template <-> PCUIC translations defined
mattam82 Jan 11, 2021
dc07622
Main infrastructure lemmas on contexts in cases proven
mattam82 Jan 11, 2021
2fe7460
Updated SigmaCalculus proofs
mattam82 Jan 12, 2021
5cca998
WIP in equality, now needing context equality
mattam82 Jan 12, 2021
13d4718
Updated Equality
mattam82 Jan 12, 2021
cafa9de
WIP in simplifying reduction
mattam82 Jan 12, 2021
dd0481f
Updated Typing to add new context conversion premisses
mattam82 Jan 13, 2021
7db4e9b
WeakeningEnv and Nameless updated
mattam82 Jan 13, 2021
c2be4d0
Move EqDec instance for Ast.term away from Reflect, so as not to poll…
mattam82 Jan 13, 2021
e803b97
Fix module includes to avoid growing rewrite databases for nothing
mattam82 Jan 13, 2021
e358ebe
Adapted PCUICNormal
mattam82 Jan 13, 2021
51005a2
WIP in PCUICClosed
mattam82 Jan 14, 2021
0df06e7
Updated Closed
mattam82 Jan 14, 2021
5d44820
Fully adapted PCUICNameless
mattam82 Jan 14, 2021
1173229
Adapted OnFreeVars
mattam82 Jan 14, 2021
dd68d3c
Adapt PCUICUnivSubstitution
mattam82 Jan 14, 2021
1a304a5
Adapted PCUICRename
mattam82 Jan 15, 2021
02827eb
Updated instantiation and substitution
mattam82 Jan 15, 2021
8dbf957
Need a new reduction rule on contexts as expected
mattam82 Jan 15, 2021
94bab92
WIP adapting Reduction to new reduction rules on contexts in cases
mattam82 Jan 15, 2021
8d10ecc
Updating UnivSubstitution
mattam82 Jan 16, 2021
3474c64
WIP in reduction is good
mattam82 Jan 16, 2021
a4f294a
Complete the theory of context reduction
mattam82 Jan 17, 2021
af59042
Updated upto instantiation and normal
mattam82 Jan 17, 2021
1b8909d
WIP lifting parallel reduction to new case context reductions
mattam82 Jan 17, 2021
beae36c
Substitutivity of parallel reduction
mattam82 Jan 17, 2021
f9135de
WIP adapting rho function
mattam82 Jan 17, 2021
c6b25ea
WIP in confluence proof
mattam82 Jan 18, 2021
289abdb
Showing that rho_ctx is stable under renaming
mattam82 Jan 19, 2021
fd4193a
WIP in parallel reduction confluence
mattam82 Jan 19, 2021
12a894a
rho match case finished
mattam82 Jan 20, 2021
87c754e
Finished updating confluence proof
mattam82 Jan 20, 2021
1771da3
WIP in finishing confluence proof
mattam82 Jan 20, 2021
f13b508
Move eq_predicate Equivalence instances in separate lemmas
mattam82 Jan 20, 2021
967bd80
Shown commnutation of eq_term and reduction
mattam82 Jan 20, 2021
dfc0c54
Need to fix problem of name preservation missing from All2_local_env
mattam82 Jan 20, 2021
8c05bb7
Before replacing All2_local_env
mattam82 Jan 20, 2021
1e33a4f
Factorize similar context relations into a general one
mattam82 Jan 21, 2021
1484164
Adapted confluence proof to new, correct context relation structure
mattam82 Jan 21, 2021
b16284a
Back in confluence with the right definitions
mattam82 Jan 21, 2021
b60ac24
Refine RedTypeIrrelevance: only body reduction matters
mattam82 Jan 21, 2021
1ba2a31
Finish confluence proofs (up to alpha-equivalence as well)
mattam82 Jan 21, 2021
3be9be0
Refine red type irrelevance: it preserves the step number
mattam82 Jan 21, 2021
6426108
WIP in Context Conversion
mattam82 Jan 21, 2021
692473a
Context Cumulativity/Conversion done
mattam82 Jan 21, 2021
e67b09a
Now in the safe zone :) Adapting conversion lemmas
mattam82 Jan 21, 2021
8ee93d4
Fix definition of comparison of declarations
mattam82 Jan 21, 2021
60a73ed
Finished conversion (one todo left)
mattam82 Jan 22, 2021
2f6fb43
In inversion
mattam82 Jan 22, 2021
4bc6923
TODOs in PCUICToTemplate
mattam82 Jan 22, 2021
f8d1a0c
Remove unused PCUICtxShape
mattam82 Jan 22, 2021
2f220ef
Before renaming fold_context
mattam82 Jan 22, 2021
61b6bb8
WIP renaming fold_context to fold_context_k
mattam82 Jan 22, 2021
45706c5
TODOs
mattam82 Jan 22, 2021
c805902
Adapted Inductives (rather easily!)
mattam82 Jan 22, 2021
3dae729
WIP in InductiveInversion
mattam82 Jan 23, 2021
801b5ad
Finished updating InductiveInversion!
mattam82 Jan 23, 2021
b1c14d4
Adapted SR (todos for Case)
mattam82 Jan 23, 2021
710919d
Adapted TemplateToPCUIC (most is todo, corrected statement of transla…
mattam82 Jan 23, 2021
d328f95
Updated Alpha conversion proof. Could be derivable from nameless (or …
mattam82 Jan 23, 2021
f7b4c00
Adapted WcbvEval entirely
mattam82 Jan 23, 2021
fad7667
Adapted SafeLemmatas, some todos on stacks left
mattam82 Jan 23, 2021
5684127
SN and cumulprop done (some todos left)
mattam82 Jan 23, 2021
888f66b
Principality with todos (does not look too hard :)
mattam82 Jan 23, 2021
00147fa
Fixed elimination (little change in statements)
mattam82 Jan 23, 2021
ca6542e
Canonicity and ConvCumInversion (with some admits)
mattam82 Jan 23, 2021
6c81863
Updated WfReduction (no todos)
mattam82 Jan 24, 2021
b6bc547
PCUICErrors updated
mattam82 Jan 24, 2021
c60a54f
Adapted EqualityDec
mattam82 Jan 24, 2021
b5950b2
Fix weird bug with make vos in WcbvEval
mattam82 Jan 24, 2021
0d696d4
Updated EqualityDec
mattam82 Jan 24, 2021
1811999
Safe Reduce updated (with todos)
mattam82 Jan 24, 2021
63cca49
Fix definitions of predicate/branch conversion
mattam82 Jan 24, 2021
2a0b944
In Safe Retyping
mattam82 Jan 24, 2021
5d01f18
Updated SafeConversion
mattam82 Jan 24, 2021
7821f3f
Finished updating safechecker (some todos left)
mattam82 Jan 25, 2021
3d8a8e8
Finished with the checker
mattam82 Jan 25, 2021
744d46d
Updated erasure (with some todos)
mattam82 Jan 25, 2021
8beb451
Update PCUICConversion, PCUICNormal, PCUICConvCumInversion
jakobbotsch Jan 26, 2021
d684cce
Update safe reduction soundness, still missing completeness
jakobbotsch Jan 27, 2021
ad72f4a
Remove unneeded file
mattam82 Jan 25, 2021
3d5c348
Update reification/quoting of inductives and cases
mattam82 Jan 27, 2021
675fbda
Remove spurious Locate command
mattam82 Jan 27, 2021
309a3f5
Add a utility function in AstUtils to go from the old representation …
mattam82 Jan 27, 2021
22cfd3f
All plugins compile
mattam82 Jan 27, 2021
fcae1e0
Add monad_utils as a dependency to the template monad plugin (useful …
mattam82 Jan 27, 2021
4a97025
Adapted translations (todo in param_original, wrong on case and induc…
mattam82 Jan 27, 2021
16c25e5
Add convenience constructors in AstUtils for building inductive and c…
mattam82 Jan 27, 2021
ccecc44
Fix the test-suite, and improve Pretty to print environments
mattam82 Jan 27, 2021
6f81b2c
Fix test-suite scripts
mattam82 Jan 27, 2021
ebde62a
A bug revealed by the safe checker, probably in reification
mattam82 Jan 27, 2021
fdbb0c6
Fix an order bug in iota_red! The arguments where substituted in the …
mattam82 Jan 28, 2021
c34dbb8
Params were substituted in the wrong order in case contexts too, fixed
mattam82 Jan 28, 2021
f571a5e
Better printer for type-checking/conversion errors
mattam82 Jan 28, 2021
dfb9f4a
SafeChecker tests passing again
mattam82 Jan 28, 2021
51ba714
Finally everything compiles
mattam82 Jan 28, 2021
a3c3a5f
Finish safe reduction
jakobbotsch Jan 28, 2021
fc66073
New ctx_inst hypothesis in Typing
mattam82 Jan 28, 2021
6151fe9
Finished validity proof
mattam82 Jan 29, 2021
cabe334
Also include the (derivable) consistent_instance_ext hyp in cases for…
mattam82 Jan 29, 2021
f8ddf7c
Renaming of validity_term to validity
mattam82 Jan 29, 2021
19eae80
Update PCUICSafeLemmata, various refactorings
jakobbotsch Feb 1, 2021
6866edc
Add a lemma relating typing_spine and ctx_inst
mattam82 Feb 1, 2021
836228f
Prove lemmas showing ctx_inst plays well with cumulativity of inducti…
mattam82 Feb 2, 2021
68cff52
Update safe conversion for new representation
jakobbotsch Feb 5, 2021
269313f
Some cleanup
jakobbotsch Feb 8, 2021
9e5392d
Fix error
jakobbotsch Feb 8, 2021
3a6d451
Update case inversion data and fix some todos
jakobbotsch Feb 9, 2021
54b814b
Shorten some lemmas in Sigma-Calculus using the algebraic identities
mattam82 Feb 3, 2021
3487e11
Move subst_consn_lt' to sigma calculus
mattam82 Feb 3, 2021
ed91b57
Simplify closed_subst_map_lift proof using sigma-calculus instead of …
mattam82 Feb 3, 2021
fabaaed
Minor refactorings in sigma-calculus proofs
mattam82 Feb 3, 2021
223b5f2
WIP in inductive inversion
mattam82 Feb 6, 2021
8e88469
WIP in typing of branches still.
mattam82 Feb 9, 2021
8560127
Fix duplication in conversion, and add missing injectivity of product…
mattam82 Feb 9, 2021
ce09486
Finally finished build_branches_types_wt proof, using more general le…
mattam82 Feb 9, 2021
6ccd915
PCUICEqualityDec moved to PCUIC for now
mattam82 Feb 9, 2021
a9fc669
finish aux lemma and cleanup PCUICInductiveInversion
mattam82 Feb 9, 2021
364f8ee
Fix broken install of template-coq as some files are no longer needed
mattam82 Feb 9, 2021
5fbcc40
More fixes for the safechecker and erasure plugins
mattam82 Feb 9, 2021
5daa2f6
WIP in SR, much simpler now
mattam82 Feb 10, 2021
31ca371
Before trying subst_app_simpl instead
mattam82 Feb 10, 2021
c3e2da3
Finished and cleaned up iota reduction type preservation
mattam82 Feb 11, 2021
75393b0
Checked that congruence for params can be proved without changing the…
mattam82 Feb 11, 2021
bb333db
Fix typing rule for SR (equivalent under context conversion)
mattam82 Feb 11, 2021
48e75f8
Almost done in SR, only a refactoring is needed to avoid duplication,…
mattam82 Feb 12, 2021
fab0cae
Refactored wf_case_branches_types for reuse in SR proof
mattam82 Feb 12, 2021
8d1c85d
Finished Subject Reduction for cases!
mattam82 Feb 12, 2021
8b06578
Admit free subject reduction proof
mattam82 Feb 13, 2021
f748140
Refactorings to finish PCUICAlpha
mattam82 Feb 13, 2021
c2167f0
Refactor proofs so that alpha-conversion is not needed for PCUICInduc…
mattam82 Feb 13, 2021
aeab3a6
Complete alpha-conversion proof
mattam82 Feb 14, 2021
5c3255f
Cleaned up notations in PCUICAlpha, move generic lemmas up
mattam82 Feb 14, 2021
32b9b75
More move of generic lemmas back in the prelude
mattam82 Feb 14, 2021
69f7030
Minor refactorings
mattam82 Feb 15, 2021
9e4600e
Fill TODOs in CumulProp and Principality.
mattam82 Feb 15, 2021
7547aac
Remove all TODOs in WfUniverse
mattam82 Feb 16, 2021
853b6c5
No more todos in PCUIC except for the correctness proofs of translations
mattam82 Feb 16, 2021
876c0aa
Cleanup PCUICElimination, removing old proofs
mattam82 Feb 16, 2021
01dcee1
Fix script in canonicity, len is more robust now
mattam82 Feb 16, 2021
f936a16
Fix script
mattam82 Feb 16, 2021
06f8089
Definition of weak-head-reduction and proof of unicity of derivations
mattam82 Feb 16, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Cleaned up notations in PCUICAlpha, move generic lemmas up
mattam82 committed Feb 14, 2021
commit 5c3255f22c4f31d3dd50ef0f5b65eee9ee80ed30
310 changes: 167 additions & 143 deletions pcuic/theories/PCUICAlpha.v
Original file line number Diff line number Diff line change
@@ -1,19 +1,99 @@
(* Distributed under the terms of the MIT license. *)
From Coq Require Import ssreflect.
From Coq Require Import ssreflect CRelationClasses CMorphisms.
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
PCUICLiftSubst PCUICTyping PCUICWeakening PCUICCumulativity PCUICEquality
PCUICConversion PCUICContextConversion PCUICValidity PCUICArities PCUICSpine
PCUICInductives PCUICInductiveInversion.
From Equations Require Import Equations.


(* TODO MOVE *)
Lemma Forall2_eq :
forall A (l l' : list A),
Forall2 eq l l' ->
l = l'.
Proof.
intros A l l' h.
induction h.
- reflexivity.
- f_equal. all: auto.
Qed.

Lemma All2_trans' {A B C}
(P : A -> B -> Type) (Q : B -> C -> Type) (R : A -> C -> Type)
(H : forall x y z, P x y × Q y z -> R x z) {l1 l2 l3}
: All2 P l1 l2 -> All2 Q l2 l3 -> All2 R l1 l3.
Proof.
induction 1 in l3 |- *.
- inversion 1; constructor.
- inversion 1; subst. constructor; eauto.
Qed.

Lemma All2_map_left_inv {A B C} (P : A -> B -> Type) (l : list C) (f : C -> A) l' :
All2 P (map f l) l' -> All2 (fun x => P (f x)) l l'.
Proof.
rewrite -{1}(map_id l').
intros. now eapply All2_map_inv in X.
Qed.

Lemma All2i_All2_All2i_All2i {A B C n} {P : nat -> A -> B -> Type} {Q : B -> C -> Type} {R : nat -> A -> C -> Type}
{S : nat -> A -> C -> Type} {l l' l''} :
All2i P n l l' ->
All2 Q l' l'' ->
All2i R n l l'' ->
(forall n x y z, P n x y -> Q y z -> R n x z -> S n x z) ->
All2i S n l l''.
Proof.
intros a b c H.
induction a in l'', b, c |- *; depelim b; depelim c; try constructor; auto.
eapply H; eauto.
Qed.

(* Alpha convertible terms and contexts have the same typings *)

Implicit Types cf : checker_flags.

Notation "`≡α`" := upto_names.
Infix "≡α" := upto_names (at level 60).
Notation "`≡Γ`" := (eq_context_upto [] eq eq).
Infix "≡Γ" := (eq_context_upto [] eq eq) (at level 20, no associativity).

Lemma R_universe_instance_eq {u u'} : R_universe_instance eq u u' -> u = u'.
Proof.
intros H.
apply Forall2_eq in H. apply map_inj in H ; revgoals.
{ apply Universe.make_inj. }
subst. constructor ; auto.
Qed.

Lemma valid_constraints_empty {cf} i : valid_constraints (empty_ext []) (subst_instance_cstrs i (empty_ext [])).
Proof.
red. destruct check_univs => //.
Qed.

Definition upto_names_ctx := eq_context_upto [] eq eq.
Instance upto_names_terms_refl : CRelationClasses.Reflexive (All2 `≡α`).
Proof. intro; apply All2_refl; reflexivity. Qed.

Infix "≡Γ" := upto_names_ctx (at level 60).
Lemma eq_term_upto_univ_it_mkLambda_or_LetIn Σ Re Rle :
RelationClasses.Reflexive Re ->
Proper (eq_context_upto Σ Re Re ==> eq_term_upto_univ Σ Re Rle ==> eq_term_upto_univ Σ Re Rle) it_mkLambda_or_LetIn.
Proof.
intros he Γ Δ eq u v h.
induction eq in u, v, h, he |- *.
- assumption.
- simpl. cbn. apply IHeq => //.
destruct p; cbn; constructor ; tas; try reflexivity.
Qed.

Lemma eq_context_upto_empty_impl {cf} {Σ : global_env_ext} ctx ctx' :
ctx ≡Γ ctx' ->
eq_context_upto Σ (eq_universe Σ) (eq_universe Σ) ctx ctx'.
Proof.
intros; eapply All2_fold_impl; tea.
intros ???? []; constructor; subst; auto;
eapply eq_term_upto_univ_empty_impl; tea; tc.
Qed.

Section Alpha.
Context {cf:checker_flags}.
@@ -42,7 +122,6 @@ Section Alpha.
destruct IHi as [s h].
+ inversion hΓ. all: auto.
+ exists s.
unfold PCUICTerm.tSort. (* TODO Why do I have to do this? *)
change (tSort s) with (lift0 1 (lift0 (S i) (tSort s))).
rewrite simpl_lift0.
eapply PCUICWeakening.weakening with (Γ' := [ c ]).
@@ -77,18 +156,6 @@ Section Alpha.
- apply nth_error_Some_length in h. assumption.
Qed.

(* TODO MOVE *)
Lemma Forall2_eq :
forall A (l l' : list A),
Forall2 eq l l' ->
l = l'.
Proof.
intros A l l' h.
induction h.
- reflexivity.
- f_equal. all: auto.
Qed.

Lemma decompose_app_upto {Σ Re Rle x y hd tl} :
eq_term_upto_univ Σ Re Rle x y ->
decompose_app x = (hd, tl) ->
@@ -107,21 +174,11 @@ Section Alpha.
inv eqh; simpl in *; try discriminate; auto.
Qed.

Lemma All2_trans' {A B C}
(P : A -> B -> Type) (Q : B -> C -> Type) (R : A -> C -> Type)
(H : forall x y z, P x y × Q y z -> R x z) {l1 l2 l3}
: All2 P l1 l2 -> All2 Q l2 l3 -> All2 R l1 l3.
Proof.
induction 1 in l3 |- *.
- inversion 1; constructor.
- inversion 1; subst. constructor; eauto.
Qed.

Lemma decompose_prod_assum_upto_names' ctx ctx' x y :
eq_context_upto [] eq eq ctx ctx' -> upto_names' x y ->
ctx ≡Γ ctx' -> upto_names' x y ->
let (ctx0, x0) := decompose_prod_assum ctx x in
let (ctx1, x1) := decompose_prod_assum ctx' y in
eq_context_upto [] eq eq ctx0 ctx1 * upto_names' x0 x1.
ctx0 ≡Γ ctx1 * upto_names' x0 x1.
Proof.
induction x in ctx, ctx', y |- *; intros eqctx eqt; inv eqt; simpl;
try split; auto; try constructor; auto.
@@ -183,7 +240,7 @@ Section Alpha.

Lemma upto_names_check_cofix mfix mfix' :
All2 (fun x y : def term =>
(upto_names' (dtype x) (dtype y) × upto_names' (dbody x) (dbody y))
(dtype x ≡α dtype y × dbody x ≡α dbody y)
× rarg x = rarg y) mfix mfix' ->
map check_one_cofix mfix = map check_one_cofix mfix'.
Proof.
@@ -217,87 +274,97 @@ Section Alpha.
Qed.

Lemma eq_context_upto_conv_context_rel {Σ : global_env_ext} {wfΣ : wf Σ} (Γ Δ Δ' : context) :
eq_context_upto [] eq eq Δ Δ' ->
Δ ≡Γ Δ' ->
conv_context_rel Σ Γ Δ Δ'.
Proof.
intros eq.
eapply All2_fold_impl; tea.
intros ???? []; constructor; auto; now constructor; apply upto_names_impl_eq_term.
Qed.
Lemma R_universe_instance_eq {u u'} : R_universe_instance eq u u' -> u = u'.

Lemma eq_context_upto_map2_set_binder_name Σ pctx pctx' Γ Δ :
pctx ≡Γ pctx' ->
eq_context_upto Σ eq eq Γ Δ ->
eq_context_upto Σ eq eq
(map2 set_binder_name (forget_types pctx) Γ)
(map2 set_binder_name (forget_types pctx') Δ).
Proof.
intros eqp.
induction 1 in pctx, pctx', eqp |- *.
- induction eqp; cbn; constructor.
- depelim eqp. simpl. constructor.
simpl. constructor; auto.
destruct c, p; constructor; auto.
Qed.

Lemma eq_context_upto_lift_context Σ Re Rle :
RelationClasses.subrelation Re Rle ->
forall u v n k,
eq_context_upto Σ Re Rle u v ->
eq_context_upto Σ Re Rle (lift_context n k u) (lift_context n k v).
Proof.
intros H.
apply Forall2_eq in H. apply map_inj in H ; revgoals.
{ apply Universe.make_inj. }
subst. constructor ; auto.
intros re u v n k.
induction 1.
- constructor.
- rewrite !lift_context_snoc; constructor; eauto.
depelim p; constructor; simpl; intuition auto;
rewrite -(length_of X);
apply eq_term_upto_univ_lift; auto.
Qed.

Lemma case_predicate_context_equiv Σ ind mdecl idecl p p' :
Lemma eq_context_upto_subst_instance Σ :
forall u v i,
valid_constraints (global_ext_constraints Σ)
(subst_instance_cstrs i Σ) ->
eq_context_upto Σ eq eq u v ->
eq_context_upto Σ eq eq (subst_instance i u) (subst_instance i v).
Proof.
intros u v i vc.
induction 1.
- constructor.
- rewrite !PCUICUnivSubst.subst_instance_cons. constructor; eauto.
depelim p; constructor; simpl; intuition auto.
eapply (PCUICUnivSubstitution.eq_term_upto_univ_subst_preserved Σ (fun _ => eq) (fun _ => eq)).
intros x y u v ? ? ->; reflexivity.
intros x y u v ? ? ->; reflexivity. exact vc.
assumption.
eapply (PCUICUnivSubstitution.eq_term_upto_univ_subst_preserved Σ (fun _ => eq) (fun _ => eq)).
intros x y u v ? ? ->; reflexivity.
intros x y u v ? ? ->; reflexivity. exact vc.
assumption.
eapply (PCUICUnivSubstitution.eq_term_upto_univ_subst_preserved Σ (fun _ => eq) (fun _ => eq)).
intros x y u v ? ? ->; reflexivity.
intros x y u v ? ? ->; reflexivity. exact vc.
assumption.
Qed.

Lemma case_predicate_context_equiv ind mdecl idecl p p' :
eq_predicate upto_names' eq p p' ->
eq_context_upto Σ eq eq
eq_context_upto [] eq eq
(case_predicate_context ind mdecl idecl p)
(case_predicate_context ind mdecl idecl p').
Proof.
intros [eqpars [eqinst [eqctx eqret]]].
rewrite /case_predicate_context /case_predicate_context_gen.
Admitted.

Lemma eq_context_upto_lift_context Σ Re Rle :
RelationClasses.subrelation Re Rle ->
forall u v n k,
eq_context_upto Σ Re Rle u v ->
eq_context_upto Σ Re Rle (lift_context n k u) (lift_context n k v).
Proof.
intros re u v n k.
induction 1.
- constructor.
- rewrite !lift_context_snoc; constructor; eauto.
depelim p; constructor; simpl; intuition auto;
rewrite -(length_of X);
apply eq_term_upto_univ_lift; auto.
Qed.
(*
Lemma upto_names_subst_instance Σ u :
valid_constraints (global_ext_constraints Σ) (subst_instance_cstrs u Σ) ->
upto_names*)

Lemma eq_context_upto_subst_instance Σ :
forall u v i,
valid_constraints (global_ext_constraints Σ)
(subst_instance_cstrs i Σ) ->
eq_context_upto Σ eq eq u v ->
eq_context_upto Σ eq eq (subst_instance i u) (subst_instance i v).
Proof.
intros u v i vc.
induction 1.
- constructor.
- rewrite !PCUICUnivSubst.subst_instance_cons. constructor; eauto.
depelim p; constructor; simpl; intuition auto.
eapply (PCUICUnivSubstitution.eq_term_upto_univ_subst_preserved Σ (fun _ => eq) (fun _ => eq)).
intros x y u v ? ? ->; reflexivity.
intros x y u v ? ? ->; reflexivity. exact vc.
assumption.
eapply (PCUICUnivSubstitution.eq_term_upto_univ_subst_preserved Σ (fun _ => eq) (fun _ => eq)).
intros x y u v ? ? ->; reflexivity.
intros x y u v ? ? ->; reflexivity. exact vc.
assumption.
eapply (PCUICUnivSubstitution.eq_term_upto_univ_subst_preserved Σ (fun _ => eq) (fun _ => eq)).
intros x y u v ? ? ->; reflexivity.
intros x y u v ? ? ->; reflexivity. exact vc.
assumption.
Qed.

Lemma valid_constraints_empty i : valid_constraints (empty_ext []) (subst_instance_cstrs i (empty_ext [])).
Proof.
red. destruct check_univs => //.
Qed.
apply eq_context_upto_map2_set_binder_name => //.
rewrite /pre_case_predicate_context_gen.
eapply R_universe_instance_eq in eqinst. rewrite -eqinst.
constructor.
- apply eq_context_upto_subst_context; tea; tc.
reflexivity.
now apply All2_rev.
- constructor; simpl; try reflexivity.
eapply eq_term_upto_univ_mkApps. reflexivity.
apply All2_app; [|reflexivity].
eapply All2_map. eapply (All2_impl eqpars).
intros. now eapply eq_term_upto_univ_lift.
Qed.

Lemma case_branch_context_equiv ind mdecl p p' bctx bctx' cdecl :
eq_predicate upto_names' eq p p' ->
eq_context_upto [] eq eq bctx bctx' ->
eq_context_upto [] eq eq
(case_branch_context ind mdecl p (forget_types bctx) cdecl)
(case_branch_context ind mdecl p' (forget_types bctx') cdecl).
bctx ≡Γ bctx' ->
(case_branch_context ind mdecl p (forget_types bctx) cdecl) ≡Γ
(case_branch_context ind mdecl p' (forget_types bctx') cdecl).
Proof.
intros [eqpars [eqinst [eqctx eqret]]] eqctx'.
eapply R_universe_instance_eq in eqinst.
@@ -322,27 +389,6 @@ Qed.
destruct r, c as [na'' [b''|] ty']; constructor; auto; try reflexivity.
Qed.

From Coq Require Import CRelationClasses CMorphisms.
Lemma eq_term_upto_univ_it_mkLambda_or_LetIn Σ Re Rle :
RelationClasses.Reflexive Re ->
Proper (eq_context_upto Σ Re Re ==> eq_term_upto_univ Σ Re Rle ==> eq_term_upto_univ Σ Re Rle) it_mkLambda_or_LetIn.
Proof.
intros he Γ Δ eq u v h.
induction eq in u, v, h, he |- *.
- assumption.
- simpl. cbn. apply IHeq => //.
destruct p; cbn; constructor ; tas; try reflexivity.
Qed.

Lemma eq_context_upto_empty_impl {Σ : global_env_ext} ctx ctx' :
eq_context_upto [] eq eq ctx ctx' ->
eq_context_upto Σ (eq_universe Σ) (eq_universe Σ) ctx ctx'.
Proof.
intros; eapply All2_fold_impl; tea.
intros ???? []; constructor; subst; auto;
eapply eq_term_upto_univ_empty_impl; tea; tc.
Qed.

Lemma case_branch_type_equiv (Σ : global_env_ext) ind mdecl idecl p p' br br' c cdecl :
eq_predicate upto_names' eq p p' ->
bcontext br ≡Γ bcontext br' ->
@@ -379,26 +425,6 @@ Qed.
+ eapply All2_refl. reflexivity.
Qed.

Lemma All2_map_left_inv {A B C} (P : A -> B -> Type) (l : list C) (f : C -> A) l' :
All2 P (map f l) l' -> All2 (fun x => P (f x)) l l'.
Proof.
rewrite -{1}(map_id l').
intros. now eapply All2_map_inv in X.
Qed.

Lemma All2i_All2_All2i_All2i {A B C n} {P : nat -> A -> B -> Type} {Q : B -> C -> Type} {R : nat -> A -> C -> Type}
{S : nat -> A -> C -> Type} {l l' l''} :
All2i P n l l' ->
All2 Q l' l'' ->
All2i R n l l'' ->
(forall n x y z, P n x y -> Q y z -> R n x z -> S n x z) ->
All2i S n l l''.
Proof.
intros a b c H.
induction a in l'', b, c |- *; depelim b; depelim c; try constructor; auto.
eapply H; eauto.
Qed.

Lemma typing_alpha :
forall Σ Γ u v A,
wf Σ.1 ->
@@ -840,14 +866,14 @@ Qed.

Lemma eq_term_upto_univ_napp_0 n t t' :
eq_term_upto_univ_napp [] eq eq n t t' ->
upto_names' t t'.
t ≡α t'.
Proof.
apply eq_term_upto_univ_empty_impl; typeclasses eauto.
Qed.

Lemma upto_names_eq_term_refl Σ Re n t t' :
RelationClasses.Reflexive Re ->
upto_names' t t' ->
t ≡α t' ->
eq_term_upto_univ_napp Σ Re Re n t t'.
Proof.
intros.
@@ -863,7 +889,7 @@ Qed.
RelationClasses.Transitive Rle ->
RelationClasses.subrelation Re Rle ->
eq_term_upto_univ_napp Σ Re Rle napp t u ->
forall t' u', t ≡ t' -> u ≡ u' ->
forall t' u', t ≡α t' -> u ≡α u' ->
eq_term_upto_univ_napp Σ Re Rle napp t' u'.
Proof.
intros.
@@ -877,22 +903,20 @@ Qed.
Qed.

Lemma upto_names_leq_term Σ φ t u t' u'
: t ≡ t' -> u ≡ u' -> leq_term Σ φ t u -> leq_term Σ φ t' u'.
: t ≡α t' -> u ≡α u' -> leq_term Σ φ t u -> leq_term Σ φ t' u'.
Proof.
intros; eapply upto_names_eq_term_upto_univ; try eassumption; tc.
Qed.

Lemma upto_names_eq_term Σ φ t u t' u'
: t ≡ t' -> u ≡ u' -> eq_term Σ φ t u -> eq_term Σ φ t' u'.
: t ≡α t' -> u ≡α u' -> eq_term Σ φ t u -> eq_term Σ φ t' u'.
Proof.
intros; eapply upto_names_eq_term_upto_univ; tea; tc.
Qed.

Definition upto_names_decl := eq_decl_upto_gen [] eq eq.

Lemma destArity_alpha Γ u v ctx s :
destArity Γ u = Some (ctx, s) ->
u ≡ v ->
u ≡α v ->
∑ ctx', destArity Γ v = Some (ctx', s) × ctx ≡Γ ctx'.
Proof.
induction u in v, Γ, ctx, s |- *; cbn; try discriminate.
@@ -950,7 +974,7 @@ Qed.
Lemma isType_alpha Σ Γ u v :
wf Σ.1 ->
isType Σ Γ u ->
u ≡ v ->
u ≡α v ->
isType Σ Γ v.
Proof.
intros hΣ [s Hs] eq.
@@ -960,7 +984,7 @@ Qed.
Lemma isWfArity_alpha Σ Γ u v :
wf Σ.1 ->
isWfArity Σ Γ u ->
u ≡ v ->
u ≡α v ->
isWfArity Σ Γ v.
Proof.
intros hΣ [isTy [ctx [s X1]]] e.