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

Stack overflow 8.17 #1017

Closed
wants to merge 104 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
104 commits
Select commit Hold shift + click to select a range
1a7d230
improved auto goal selection (#737)
mrhaandi Jul 18, 2022
7d1b643
prepare for https://github.com/coq/coq/pull/16289 (#734)
mrhaandi Jul 18, 2022
2e1085a
Adapt w.r.t. coq/coq#16442.
ppedrot Sep 14, 2022
6219522
ML fixes
mattam82 Sep 20, 2022
7399921
Adapt to Coq 8.17
mattam82 Apr 13, 2023
0d08380
Update opam packages
mattam82 Apr 13, 2023
6f72fe9
Update github action coq version
mattam82 Apr 13, 2023
83cea47
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
mattam82 Apr 14, 2023
66e7d31
Usage for make-opam-files
mattam82 Apr 14, 2023
76e8e48
Fix dep in opam file
mattam82 Apr 14, 2023
ea7b244
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
mattam82 Apr 17, 2023
4b975ae
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
mattam82 Apr 18, 2023
66f6857
Fix due to high priority existT hint in core
mattam82 Apr 18, 2023
f867f01
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
mattam82 Apr 19, 2023
e61cd19
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
mattam82 Apr 19, 2023
736ac17
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
mattam82 Apr 20, 2023
1f9ed65
Update install instructions for Coq 8.17
mattam82 Apr 20, 2023
c27c302
Merge branch 'coq-8.16' into coq-8.17
mattam82 Apr 22, 2023
198e202
Fix sprop_level/prop_level requring lazy evaluation
mattam82 May 5, 2023
f91a1e7
close some computational obligations with defined in erase_global_decls
yforster May 5, 2023
e578a02
Move nix actions away
mattam82 May 9, 2023
bb34a12
Merge pull request #961 from yforster/fix-qed-problem
mattam82 May 9, 2023
14ad024
Invariants in named recursion rule (#967)
yforster Jun 2, 2023
c065ed6
Update Makefile to install erasure plugin
mattam82 Jun 2, 2023
e0794e3
Fix sneaky, useless Prop <= Type use that was breaking certified erasure
mattam82 Jun 28, 2023
3e0f857
Bump actions/checkout from 3 to 4 (#978)
dependabot[bot] Sep 4, 2023
adba794
improve stengthening to get cumul info on type
tabareau Sep 26, 2023
9fd6f61
more general strengthening
tabareau Sep 26, 2023
46be926
Merge pull request #985 from MetaCoq/improve-strengthening
tabareau Sep 27, 2023
be44477
remove parameters in firstorder inductive types
tabareau Sep 27, 2023
a152eec
Merge pull request #986 from MetaCoq/remove-parameters-in-firstorder-…
tabareau Sep 28, 2023
dce0b9e
split out verified erasure pipeline
yforster Jul 6, 2023
a813bff
Add pass implementing boxes as fixpoints
yforster Jul 6, 2023
5bc51f5
adapt name pass to not consider box
yforster Jul 6, 2023
7565dd4
remove assumption
yforster Jul 6, 2023
a359961
Fix definition of Transform.t's observational equivalence preservation
mattam82 Jul 7, 2023
06ca492
prove wellformedness of annotate
yforster Jul 11, 2023
f1a2548
wellformed_annotate_env
yforster Jul 12, 2023
6a1428a
WIP stronger global weakening theorems for optimizations
mattam82 Jul 17, 2023
e09e64d
Allow modifying inductive decls in generic weakenability translation …
mattam82 Aug 21, 2023
805bbda
Prove a more precise result about erase_global_decls with dependencies
mattam82 Aug 23, 2023
8710ece
No need for ext proof for erasure
mattam82 Aug 28, 2023
7158506
Strenghtened program extension preservation
mattam82 Aug 28, 2023
3856b00
Progress on pipeline theorem proof, main argument remains
mattam82 Aug 28, 2023
71819e7
Main argument of the erasure with dependencies proof
mattam82 Aug 29, 2023
93395bf
Finish the proofs in ErasureFunction
mattam82 Aug 30, 2023
80055db
Finished proof of firstorder correctness for erase_pcuic_program
mattam82 Aug 31, 2023
0934fc0
Modify Transform class to allow showing preservation of fo values com…
mattam82 Aug 31, 2023
1f1248d
Proved most of the fo preservation of the lambdabox pipeline
mattam82 Sep 1, 2023
0e5938a
Finish main erasure correctness proof. Need to move expand_lets reaso…
mattam82 Sep 7, 2023
915ce93
We're missing preservation of eta-expandedness by reduction in PCUIC...
mattam82 Sep 8, 2023
f169916
Prove preservation of expansion by reduction using a custom reduction…
mattam82 Sep 11, 2023
2f5fed3
Finished preservation of expansion proof
mattam82 Sep 12, 2023
681a382
Refactor a bit, work on side conditions for let expansion
mattam82 Sep 12, 2023
b072acf
Filled all proofs in ErasureCorrectness
mattam82 Sep 13, 2023
708302f
Cleanup a bit, remain only normalization side-conditions
mattam82 Sep 13, 2023
a0dc628
Fix erasure plugin compilation
mattam82 Sep 13, 2023
487cdf5
Cleanup
mattam82 Sep 15, 2023
dfb03d1
Minor fixes
mattam82 Oct 2, 2023
f2b1cc0
Fix after rebase
mattam82 Oct 3, 2023
357e8a7
Fix test suite
mattam82 Oct 3, 2023
3733e67
Merge pull request #987 from MetaCoq/verified_erasure_pipeline
mattam82 Oct 3, 2023
1dc7961
add not_isErasable lemma in EArities
tabareau Oct 10, 2023
65e8a93
Merge pull request #990 from MetaCoq/not_isErasable
tabareau Oct 10, 2023
241dd7f
Merge remote-tracking branch 'origin/coq-8.16' into coq-8.17
yforster Oct 16, 2023
34c831e
fix Makefile
yforster Oct 16, 2023
1e3d82d
Merge pull request #992 from MetaCoq/coq-8.17-updates-8.16
yforster Oct 16, 2023
18a24e5
use names in EAst.t
tabareau Oct 26, 2023
79f7454
Merge pull request #997 from MetaCoq/use-names-in-EAst
tabareau Oct 26, 2023
f7d27f7
linearize case
yforster Oct 25, 2023
7d58a86
add install-plugins target in Makefile
yforster Oct 25, 2023
f8aba7c
move implement_box_transformation to coq-malfunction
yforster Oct 25, 2023
6d98589
eliminate race condition for opam compilation
yforster Nov 1, 2023
e649edb
disable quick target in CI - it is not quicker
yforster Nov 1, 2023
b33a9bd
fix Makefile and opam files
yforster Nov 1, 2023
a6b7428
Show that applications of eta-expanded functions are preserved
mattam82 Oct 20, 2023
9ed43d7
Prove app preservation for erase and let expansion
mattam82 Oct 23, 2023
0def703
WIP on normal predicate
mattam82 Oct 26, 2023
1f4249d
Definition of normal forms and proof that they reduce only to themselves
mattam82 Nov 9, 2023
537e248
Use normal form characterization in nisErasable
mattam82 Nov 9, 2023
84a264f
Preservation of applications for proven for the whole pipeline
mattam82 Nov 14, 2023
64b8171
Cleanup ErasureCorrectness
mattam82 Nov 15, 2023
27d6ad2
Fix unqualified, ambiguous imports
mattam82 Nov 15, 2023
b63f41a
Merge pull request #1013 from MetaCoq/compile-pipeline-app
mattam82 Nov 15, 2023
b4ef021
separate extends and extends_eprogram
tabareau Nov 14, 2023
3a954d5
prove missing lemmas of the pipeline
tabareau Nov 14, 2023
f941495
fix after rebase
tabareau Nov 15, 2023
6eef155
Merge pull request #1014 from MetaCoq/transform-extends-split
tabareau Nov 15, 2023
4566665
Support primitive array terms
mattam82 Oct 30, 2023
ed544ea
WIP up to confluence for arrays
mattam82 Nov 6, 2023
c86a3a8
Alpha-conv and validity done
mattam82 Nov 6, 2023
26779c7
Proved subject reduction for arrays
mattam82 Nov 7, 2023
a7af745
Adapted all of PCUIC to primitive arrays (and in general term contain…
mattam82 Nov 7, 2023
e93c39c
Done with template <-> PCUIC. Working on safe checker
mattam82 Nov 17, 2023
3ee01a3
Update PCUICPosition to include arrays
mattam82 Nov 20, 2023
67bba98
Updatet SafeConversion to arrays
mattam82 Nov 21, 2023
51cb57d
Typechecking of arrays
mattam82 Nov 21, 2023
69c1f05
In erasure, must update solve_all to automate proofs
mattam82 Nov 24, 2023
8ecbd0e
WIP in erasure of arrays
mattam82 Nov 23, 2023
3354847
Adapt erasure for primitive arrays
mattam82 Nov 24, 2023
8b4d7a9
Disable quotation module build
mattam82 Nov 24, 2023
133b5ad
Fixes after rebase
mattam82 Nov 24, 2023
2fc21e5
Adapted extraction correctness, only remaining wf_glob proofs
mattam82 Nov 27, 2023
5127430
WIP on wellformedness proof
mattam82 Nov 28, 2023
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
Support primitive array terms
mattam82 committed Nov 24, 2023

Verified

This commit was signed with the committer’s verified signature.
renovate-bot Mend Renovate
commit 45666652abfbc44e3e23289ddfa4d107a2b302af
47 changes: 34 additions & 13 deletions common/theories/Environment.v
Original file line number Diff line number Diff line change
@@ -40,51 +40,58 @@ Module Retroknowledge.
Record t := mk_retroknowledge {
retro_int63 : option kername;
retro_float64 : option kername;
retro_array : option kername;
}.

Definition empty := {| retro_int63 := None; retro_float64 := None |}.
Definition empty := {| retro_int63 := None; retro_float64 := None; retro_array := None |}.

Definition extends (x y : t) :=
option_extends x.(retro_int63) y.(retro_int63) /\
option_extends x.(retro_float64) y.(retro_float64).
option_extends x.(retro_float64) y.(retro_float64) /\
option_extends x.(retro_array) y.(retro_array).
Existing Class extends.

Definition extendsb (x y : t) :=
option_extendsb x.(retro_int63) y.(retro_int63) &&
option_extendsb x.(retro_float64) y.(retro_float64).
option_extendsb x.(retro_float64) y.(retro_float64) &&
option_extendsb x.(retro_array) y.(retro_array).

Lemma extendsT x y : reflect (extends x y) (extendsb x y).
Proof.
rewrite /extends/extendsb; do 2 case: option_extendsT; cbn; constructor; intuition.
rewrite /extends/extendsb; do 3 case: option_extendsT; cbn; constructor; intuition.
Qed.

Lemma extends_spec x y : extendsb x y <-> extends x y.
Proof.
rewrite /extends/extendsb -!option_extends_spec /is_true !Bool.andb_true_iff //=.
intuition auto.
Qed.

#[global] Instance extends_refl x : extends x x.
Proof.
split; apply option_extends_refl.
repeat split; apply option_extends_refl.
Qed.

#[global] Instance extends_trans : RelationClasses.Transitive Retroknowledge.extends.
Proof.
intros x y z [] []; split; cbn; now etransitivity; tea.
intros x y z [? []] [? []]; repeat split; cbn; now etransitivity; tea.
Qed.

#[export,program] Instance reflect_t : ReflectEq t := {
eqb x y := (x.(retro_int63) == y.(retro_int63)) &&
(x.(retro_float64) == y.(retro_float64))
(x.(retro_float64) == y.(retro_float64)) &&
(x.(retro_array) == y.(retro_array))
}.
Next Obligation.
do 2 case: eqb_spec; destruct x, y; cbn; intros; subst; constructor; congruence.
do 3 case: eqb_spec; destruct x, y; cbn; intros; subst; constructor; congruence.
Qed.

(** This operation is asymmetric; it perfers the first argument when the arguments are incompatible, but otherwise takes the join *)
Definition merge (r1 r2 : t) : t
:= {| retro_int63 := match r1.(retro_int63) with Some v => Some v | None => r2.(retro_int63) end
; retro_float64 := match r1.(retro_float64) with Some v => Some v | None => r2.(retro_float64) end |}.
; retro_float64 := match r1.(retro_float64) with Some v => Some v | None => r2.(retro_float64) end
; retro_array := match r1.(retro_array) with Some v => Some v | None => r2.(retro_array) end
|}.

Lemma extends_l_merge r1 r2
: extends r1 (merge r1 r2).
@@ -102,7 +109,8 @@ Module Retroknowledge.

Definition compatible (x y : t) : bool
:= match x.(retro_int63), y.(retro_int63) with Some x, Some y => x == y | _, _ => true end
&& match x.(retro_float64), y.(retro_float64) with Some x, Some y => x == y | _, _ => true end.
&& match x.(retro_float64), y.(retro_float64) with Some x, Some y => x == y | _, _ => true end
&& match x.(retro_array), y.(retro_array) with Some x, Some y => x == y | _, _ => true end.

Lemma extends_r_merge r1 r2
: compatible r1 r2 -> extends r2 (merge r1 r2).
@@ -836,12 +844,25 @@ Module Environment (T : Term).
match p with
| primInt => Σ.(retroknowledge).(Retroknowledge.retro_int63)
| primFloat => Σ.(retroknowledge).(Retroknowledge.retro_float64)
| primArray => Σ.(retroknowledge).(Retroknowledge.retro_array)
end.

Definition primitive_invariants (cdecl : constant_body) :=
∑ s, [/\ cdecl.(cst_type) = tSort s, cdecl.(cst_body) = None &
cdecl.(cst_universes) = Monomorphic_ctx].
Definition tImpl (dom codom : term) : term :=
tProd {| binder_name := nAnon; binder_relevance := Relevant |}
dom (lift 1 0 codom).

Definition array_uctx := ([nAnon], ConstraintSet.empty).

Definition primitive_invariants (p : prim_tag) (cdecl : constant_body) :=
match p with
| primInt | primFloat =>
∑ s, [/\ cdecl.(cst_type) = tSort s, cdecl.(cst_body) = None &
cdecl.(cst_universes) = Monomorphic_ctx]
| primArray =>
let s := Universe.make (Level.lvar 0) in
[/\ cdecl.(cst_type) = tImpl (tSort s) (tSort s), cdecl.(cst_body) = None &
cdecl.(cst_universes) = Polymorphic_ctx array_uctx]
end.

(** A context of global declarations + global universe constraints,
i.e. a global environment *)
4 changes: 2 additions & 2 deletions common/theories/Primitive.v
Original file line number Diff line number Diff line change
@@ -6,8 +6,8 @@ Local Open Scope bs.

Variant prim_tag :=
| primInt
| primFloat.
(* | primArray. *)
| primFloat
| primArray.
Derive NoConfusion EqDec for prim_tag.

Definition string_of_prim_int (i:Uint63.int) : string :=
7 changes: 4 additions & 3 deletions erasure/theories/EEtaExpandedFix.v
Original file line number Diff line number Diff line change
@@ -525,7 +525,7 @@ Section isEtaExp.
#|Γ| = k ->
nth_error mfix idx = Some d ->
closed (EAst.tFix mfix idx) ->
forallb (fun x => isLambda x.(dbody) && isEtaExp (rev_map (S ∘ rarg) mfix) x.(dbody)) mfix ->
forallb (fun x => isEtaExp (rev_map (S ∘ rarg) mfix) x.(dbody)) mfix ->
isEtaExp (Γ ++ [1 + d.(EAst.rarg)] ++ Δ) b -> isEtaExp (Γ ++ Δ) (ECSubst.csubst (EAst.tFix mfix idx) k b).
Proof using Type*.
intros Hk Hnth Hcl.
@@ -631,13 +631,14 @@ Section isEtaExp.
Qed.

Lemma isEtaExp_fixsubstl Δ mfix t :
forallb (fun x => isLambda x.(dbody) &&
forallb (fun x =>
(* isLambda x.(dbody) && *)
isEtaExp (rev_map (S ∘ rarg) mfix) x.(dbody)) mfix ->
isEtaExp ((rev_map (S ∘ rarg) mfix) ++ Δ) t ->
isEtaExp Δ (substl (fix_subst mfix) t).
Proof using Type*.
intros Hall Heta.
assert (Hcl : closed (EAst.tFix mfix 0) ). { cbn. solve_all. rtoProp; intuition auto. eapply isEtaExp_closed in H0. revert H0. now len. }
assert (Hcl : closed (EAst.tFix mfix 0) ). { cbn. solve_all. rtoProp; intuition auto. eapply isEtaExp_closed in H. revert H. now len. }
revert Hcl Hall Heta.
intros Hcl Hall Heta.
cbn in Hcl. solve_all.
18 changes: 14 additions & 4 deletions pcuic/theories/Bidirectional/BDTyping.v
Original file line number Diff line number Diff line change
@@ -124,8 +124,9 @@ Inductive infering `{checker_flags} (Σ : global_env_ext) (Γ : context) : term
| infer_Prim p prim_ty cdecl :
primitive_constant Σ (prim_val_tag p) = Some prim_ty ->
declared_constant Σ prim_ty cdecl ->
primitive_invariants cdecl ->
Σ ;;; Γ |- tPrim p ▹ tConst prim_ty []
primitive_invariants (prim_val_tag p) cdecl ->
primitive_typing_hyps checking Σ Γ p ->
Σ ;;; Γ |- tPrim p ▹ prim_type p prim_ty

with infering_sort `{checker_flags} (Σ : global_env_ext) (Γ : context) : term -> Universe.t -> Type :=
| infer_sort_Sort t T u:
@@ -196,6 +197,7 @@ Proof.
| H : checking _ _ _ _ |- _ => apply checking_size in H
| H : wf_local_bd _ _ |- _ => apply (All_local_env_sorting_size _ _ (checking_size _) (infering_sort_size _) _ _) in H
| H : wf_local_bd_rel _ _ _ |- _ => apply (All_local_rel_sorting_size (checking_size _) (infering_sort_size _) _ _) in H
| H : primitive_typing_hyps _ _ _ _ |- _ => apply (primitive_typing_hyps_size _ (checking_size _)) in H
end ;
match goal with
| H : All2i _ _ _ _ |- _ => idtac
@@ -448,8 +450,10 @@ Section BidirectionalInduction.
(forall (Γ : context) p prim_ty cdecl,
primitive_constant Σ (prim_val_tag p) = Some prim_ty ->
declared_constant Σ prim_ty cdecl ->
primitive_invariants cdecl ->
Pinfer Γ (tPrim p) (tConst prim_ty [])) ->
primitive_invariants (prim_val_tag p) cdecl ->
primitive_typing_hyps checking Σ Γ p ->
primitive_typing_hyps (fun _ => Pcheck) Σ Γ p ->
Pinfer Γ (tPrim p) (prim_type p prim_ty)) ->

(forall (Γ : context) (t T : term) (u : Universe.t),
Σ ;;; Γ |- t ▹ T ->
@@ -681,6 +685,12 @@ Section BidirectionalInduction.
cbn. lia.

- unshelve eapply HPrim; eauto.
simpl in IH.
destruct p1; constructor; eauto.
applyIH. applyIH. simpl in IH.
clear -IH. induction hvalue; constructor; eauto.
eapply (IH (check_cons _ _ _ p)). simpl; lia.
eapply IHhvalue. intros; simpl. eapply IH. simpl. lia.

- destruct i.
unshelve (eapply HiSort ; try eassumption) ; try eassumption.
46 changes: 46 additions & 0 deletions pcuic/theories/Conversion/PCUICUnivSubstitutionConv.v
Original file line number Diff line number Diff line change
@@ -190,6 +190,11 @@ Proof.
* solve_all. reflexivity.
* eapply X => //.
- solve_all. reflexivity.
- destruct p as [? []]; cbn in X; constructor; cbn; intuition eauto; cbn.
* rewrite -!subst_instance_univ_make. now eapply hRe.
* now eapply a1.
* now eapply a0.
* solve_all. eapply All_All2; tea. intuition eauto. now apply X.
Qed.

#[global]
@@ -355,6 +360,8 @@ Proof.
rewrite map_def_map_def; solve_all.
- rewrite map_map. apply All_map_eq. solve_all.
rewrite map_def_map_def; solve_all.
- rewrite !mapu_prim_compose_rew. solve_all.
intro. eapply subst_instance_level_two.
Qed.

Lemma subst_instance_two_context u1 u2 (Γ : context) :
@@ -880,6 +887,11 @@ Proof.
repeat split; simpl; eauto; solve_all.
* eapply precompose_subst_instance.
eapply R_universe_instance_impl; eauto.
- destruct p as [? []]; depelim X1; cbn in X; try constructor; intuition eauto.
* cbn. rewrite -!subst_instance_univ_make. now eapply he.
* now eapply a2.
* now eapply a0.
* cbn. solve_all.
Qed.

Lemma leq_term_subst_instance {cf : checker_flags} Σ : SubstUnivPreserved (leq_term Σ).
@@ -1442,6 +1454,7 @@ Proof.
red. split; cbn; eauto.
rewrite subst_instance_app in r0.
now rewrite <- (fix_context_subst_instance u mfix0).
- cbn. eapply array_red_val. eapply OnOne2_map. cbn. solve_all.
Qed.

Lemma subst_instance_ws_cumul_pb {cf : checker_flags} (Σ : global_env_ext) Γ u A B univs :
@@ -1819,6 +1832,30 @@ Section SubstIdentity.
simpl in lin, onu. lsets.
Qed.


Lemma consistent_instance_ext_subst_abs_level Σ decl u :
wf_ext_wk Σ ->
consistent_instance_ext Σ decl [u] ->
subst_instance_level (abstract_instance Σ.2) u = u.
Proof using Type.
intros [wfΣ onu] cu.
destruct decl.
- simpl in cu. destruct u; simpl in *; try discriminate; auto.
- destruct cu as [decl' [sizeu vc]].
clear sizeu vc.
destruct u; simpl; auto. cbn -[global_ext_levels] in decl'.
rewrite andb_true_r in decl'.
eapply LevelSet.mem_spec in decl'.
eapply in_var_global_ext in decl'; auto.
destruct (udecl_prop_in_var_poly onu decl') as [[univs csts] eq].
rewrite eq in decl' |- *. simpl in *.
rewrite mapi_unfold in decl' |- *.
eapply LevelSet_In_fold_right_add in decl'.
eapply In_unfold_inj in decl'; try congruence.
eapply (nth_error_unfold Level.lvar) in decl'.
now rewrite (nth_error_nth _ _ _ decl').
Qed.

Lemma consistent_instance_ext_subst_abs Σ decl u :
wf_ext_wk Σ ->
consistent_instance_ext Σ decl u ->
@@ -2004,6 +2041,15 @@ Section SubstIdentity.
- clear X0. eapply nth_error_all in X as [s [Hs [IHs _]]]; eauto.
- solve_all. destruct a as [s [? ?]]. solve_all.
- clear X0. eapply nth_error_all in X as [s [Hs [IHs _]]]; eauto.
- destruct p as [? []]; cbn => //. do 2 f_equal.
depelim X1. specialize (hty X2); specialize (hdef X2).
unfold mapu_array_model; destruct a; cbn -[Universe.make] in * => //=; f_equal; intuition eauto.
* destruct array_level => //.
rewrite subst_instance_univ_make in b. now injection b.
* solve_all.
- depelim X1; cbn => //=. destruct X. simp prim_type. cbn. f_equal; intuition eauto.
do 2 f_equal. cbn -[Universe.make] in b. rewrite subst_instance_univ_make in b.
now injection b.
Qed.

Lemma typed_subst_abstract_instance Σ Γ t T :
6 changes: 6 additions & 0 deletions pcuic/theories/Conversion/PCUICWeakeningConfigConv.v
Original file line number Diff line number Diff line change
@@ -97,6 +97,8 @@ Proof.
eapply All2_impl'; tea.
eapply All_impl; eauto.
cbn. intros x [? ?] y [[[? ?] ?] ?]. repeat split; eauto.
- intros h; depelim h; constructor; cbn in X; intuition eauto.
depelim e; cbn in X; constructor; intuition eauto. solve_all.
Qed.

Lemma weakening_config_cumul_gen {cf1 cf2} pb Σ Γ M N :
@@ -142,6 +144,10 @@ Proof.
* solve_all.
- eapply cumul_Fix. solve_all.
- eapply cumul_CoFix; solve_all.
- eapply cumul_Prim; solve_all.
destruct X; constructor; eauto.
* now eapply (@cmp_universe_config_impl cf1 cf2).
* solve_all.
- eapply cumul_Ind; eauto. 2:solve_all.
eapply @R_global_instance_weaken_subrel; [ .. | eassumption ].
all: repeat change (@eq_universe ?cf) with (@compare_universe cf Conv).
6 changes: 6 additions & 0 deletions pcuic/theories/Conversion/PCUICWeakeningEnvConv.v
Original file line number Diff line number Diff line change
@@ -125,6 +125,8 @@ Proof using P Pcmp cf.
eapply All2_impl'; tea.
eapply All_impl; eauto.
cbn. intros x [? ?] y [[[? ?] ?] ?]. repeat split; eauto.
- inversion 1; subst; constructor.
depelim X1; constructor; cbn in X; intuition eauto. solve_all.
Qed.

Lemma weakening_env_red1 Σ Σ' Γ M N :
@@ -198,6 +200,10 @@ Proof.
* solve_all.
- eapply cumul_Fix; solve_all.
- eapply cumul_CoFix; solve_all.
- eapply cumul_Prim; solve_all.
destruct X; constructor; eauto.
* unfold compare_universe. eapply subrel_extends_eq; tea.
* solve_all.
- eapply cumul_Ind; eauto. 2:solve_all.
eapply @R_global_instance_weaken_env. 1,2,6:eauto. all: tc.
- eapply cumul_Construct; eauto. 2:solve_all.
Loading