Improve generalized rewriting in Type and with univpoly #14137
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
SkySkimmer
reviewed
Apr 21, 2021
SkySkimmer
reviewed
Apr 21, 2021
mattam82
force-pushed
the
setoid-rewrite-type
branch
from
6a8e17d
to
4bd2ea0
Compare
|
Hey, I have detected that there were CI failures at commit 4bd2ea0 without any failure in the test-suite. |
|
@coqbot ci minimize |
|
I have initiated minimization at commit 4bd2ea0 for the suggested target ci-metacoq as requested. |
|
Error: Could not minimize file (from ci-metacoq) (full log on GitHub Actions) build log (truncated to last 26KiB; full 1.7MiB file on GitHub Actions Artifacts under
|
|
Metacoq minimization now works! Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories/PCUICSigmaCalculus.v (from ci-metacoq) (full log on GitHub Actions) Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/theories" "MetaCoq.Template" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/template-coq/build" "-top" "PCUICSigmaCalculus" "-native-compiler" "no") -*- *)
(* File reduced by coq-bug-finder from original input, then from 2424 lines to 30 lines, then from 134 lines to 2007 lines, then from 2006 lines to 201 lines, then from 291 lines to 459 lines, then from 463 lines to 248 lines, then from 337 lines to 449 lines, then from 453 lines to 257 lines, then from 337 lines to 784 lines, then from 783 lines to 277 lines, then from 356 lines to 2561 lines, then from 2544 lines to 293 lines, then from 366 lines to 779 lines, then from 781 lines to 348 lines, then from 419 lines to 458 lines, then from 462 lines to 353 lines, then from 422 lines to 626 lines, then from 628 lines to 364 lines, then from 419 lines to 502 lines, then from 504 lines to 385 lines, then from 439 lines to 1524 lines, then from 1521 lines to 421 lines, then from 470 lines to 673 lines, then from 673 lines to 437 lines, then from 481 lines to 561 lines, then from 565 lines to 456 lines, then from 460 lines to 456 lines *)
(* coqc version 8.15+alpha compiled with OCaml 4.05.0
coqtop version 8.15+alpha *)
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Require Coq.Lists.SetoidList.
Module Export MetaCoq_DOT_Template_DOT_utils_DOT_MCPrelude.
Module Export MetaCoq.
Module Export Template.
Module Export utils.
Module Export MCPrelude.
Coercion is_true : bool >-> Sortclass.
Notation "'∑' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p%type)) ..))
(at level 200, x binder, right associativity,
format "'[' '∑' '/ ' x .. y , '/ ' p ']'")
: type_scope.
End MCPrelude.
End utils.
End Template.
End MetaCoq.
End MetaCoq_DOT_Template_DOT_utils_DOT_MCPrelude.
Require Coq.ssr.ssreflect.
Require Coq.Floats.SpecFloat.
Module Export MetaCoq_DOT_Template_DOT_utils_DOT_MCRelations.
Module Export MetaCoq.
Module Export Template.
Module Export utils.
Module Export MCRelations.
Import Coq.Classes.CRelationClasses.
Infix "<~>" := iffT (at level 90).
End MCRelations.
End utils.
End Template.
End MetaCoq.
End MetaCoq_DOT_Template_DOT_utils_DOT_MCRelations.
Module Export MetaCoq_DOT_Template_DOT_utils_DOT_MCList.
Module Export MetaCoq.
Module Export Template.
Module Export utils.
Module Export MCList.
Import Coq.Lists.SetoidList.
Export ListNotations.
Notation "#| l |" := (List.length l) (at level 0, l at level 99, format "#| l |").
Definition rev {A} (l : list A) : list A :=
let fix aux (l : list A) (acc : list A) : list A :=
match l with
| [] => acc
| x :: l => aux l (x :: acc)
end
in aux l [].
Lemma nth_error_Some' {A} l n : (∑ x : A, nth_error l n = Some x) <~> n < length l.
admit.
Defined.
End MCList.
End utils.
End Template.
End MetaCoq.
End MetaCoq_DOT_Template_DOT_utils_DOT_MCList.
Module Export MetaCoq_DOT_Template_DOT_utils_DOT_MCProd.
Module Export MetaCoq.
Module Export Template.
Module Export utils.
Module Export MCProd.
Notation "x × y" := (prod x y ) (at level 80, right associativity).
Definition on_snd {A B C} (f : B -> C) (p : A * B) :=
(fst p, f (snd p)).
Definition test_snd {A B} (f : B -> bool) (p : A * B) :=
f (snd p).
End MCProd.
End utils.
End Template.
End MetaCoq.
End MetaCoq_DOT_Template_DOT_utils_DOT_MCProd.
Module Export MetaCoq.
Module Export Template.
Module Export utils.
Module Export MCUtils.
Export MetaCoq.Template.utils.MCList.
End MCUtils.
Export Coq.Bool.Bool.
Export Coq.ZArith.ZArith.
Export Coq.Strings.String.
Export Coq.Lists.List.
Export MetaCoq.Template.utils.MCUtils.
Notation "A * B" := (prod A B) : type_scope2.
Global Open Scope type_scope2.
Import Coq.Floats.SpecFloat.
Definition ident := string.
Definition dirpath := list ident.
Inductive modpath :=
| MPfile (dp : dirpath)
| MPbound (dp : dirpath) (id : ident) (i : nat)
| MPdot (mp : modpath) (id : ident).
Definition kername := modpath × ident.
Inductive name : Set :=
| nAnon
| nNamed (_ : ident).
Inductive relevance : Set := Relevant | Irrelevant.
Record binder_annot (A : Type) := mkBindAnn { binder_name : A; binder_relevance : relevance }.
Definition aname := binder_annot name.
Record inductive : Set := mkInd { inductive_mind : kername ;
inductive_ind : nat }.
Definition projection : Set := inductive * nat * nat .
Record def term := mkdef {
dname : aname;
dtype : term;
dbody : term;
rarg : nat }.
Arguments dname {term} _.
Arguments dtype {term} _.
Arguments dbody {term} _.
Arguments rarg {term} _.
Definition map_def {A B} (tyf bodyf : A -> B) (d : def A) :=
{| dname := d.(dname); dtype := tyf d.(dtype); dbody := bodyf d.(dbody); rarg := d.(rarg) |}.
Definition mfixpoint term := list (def term).
Definition test_def {A} (tyf bodyf : A -> bool) (d : def A) :=
tyf d.(dtype) && bodyf d.(dbody).
Definition uint_size := 63.
Definition uint_wB := (2 ^ (Z.of_nat uint_size))%Z.
Definition uint63_model := { z : Z | ((0 <=? z) && (z <? uint_wB))%Z }.
Definition prec := 53%Z.
Definition emax := 1024%Z.
Definition float64_model := sig (valid_binary prec emax).
Module Export Level.
Inductive t_ : Set :=
| lSet
| Level (_ : string)
| Var (_ : nat) .
Definition t := t_.
Module Export Universe.
Definition t := t_.
Module Export Instance.
Definition t : Set := list Level.t.
Module Type Term.
Parameter Inline term : Type.
Parameter Inline tRel : nat -> term.
End Term.
Module Environment (T : Term).
Import T.
Record context_decl := mkdecl {
decl_name : aname ;
decl_body : option term ;
decl_type : term
}.
Definition vass x A :=
{| decl_name := x ; decl_body := None ; decl_type := A |}.
Definition context := list context_decl.
Fixpoint reln (l : list term) (p : nat) (Γ0 : list context_decl) {struct Γ0} : list term :=
match Γ0 with
| [] => l
| {| decl_body := Some _ |} :: hyps => reln l (p + 1) hyps
| {| decl_body := None |} :: hyps => reln (tRel p :: l) (p + 1) hyps
end.
Definition to_extended_list_k Γ k := reln [] k Γ.
Definition to_extended_list Γ := to_extended_list_k Γ 0.
End Environment.
Variant prim_tag :=
| primInt
| primFloat.
Inductive prim_model (term : Type) : prim_tag -> Type :=
| primIntModel (i : uint63_model) : prim_model term primInt
| primFloatModel (f : float64_model) : prim_model term primFloat.
Definition prim_val term := ∑ t : prim_tag, prim_model term t.
Inductive term :=
| tRel (n : nat)
| tVar (i : ident)
| tEvar (n : nat) (l : list term)
| tSort (u : Universe.t)
| tProd (na : aname) (A B : term)
| tLambda (na : aname) (A t : term)
| tLetIn (na : aname) (b B t : term)
| tApp (u v : term)
| tConst (k : kername) (ui : Instance.t)
| tInd (ind : inductive) (ui : Instance.t)
| tConstruct (ind : inductive) (n : nat) (ui : Instance.t)
| tCase (indn : inductive * nat) (p c : term) (brs : list (nat * term))
| tProj (p : projection) (c : term)
| tFix (mfix : mfixpoint term) (idx : nat)
| tCoFix (mfix : mfixpoint term) (idx : nat)
| tPrim (prim : prim_val term).
Module PCUICTerm <: Term.
Definition term := term.
Definition tRel := tRel.
End PCUICTerm.
Module PCUICEnvironment := Environment PCUICTerm.
Include PCUICEnvironment.
Import Nat.
Definition shiftn k f :=
fun n => if Nat.ltb n k then n else k + (f (n - k)).
Fixpoint rename f t : term :=
match t with
| tRel i => tRel (f i)
| tEvar ev args => tEvar ev (List.map (rename f) args)
| tLambda na T M => tLambda na (rename f T) (rename (shiftn 1 f) M)
| tApp u v => tApp (rename f u) (rename f v)
| tProd na A B => tProd na (rename f A) (rename (shiftn 1 f) B)
| tLetIn na b t b' => tLetIn na (rename f b) (rename f t) (rename (shiftn 1 f) b')
| tCase ind p c brs =>
let brs' := List.map (on_snd (rename f)) brs in
tCase ind (rename f p) (rename f c) brs'
| tProj p c => tProj p (rename f c)
| tFix mfix idx =>
let mfix' := List.map (map_def (rename f) (rename (shiftn (List.length mfix) f))) mfix in
tFix mfix' idx
| tCoFix mfix idx =>
let mfix' := List.map (map_def (rename f) (rename (shiftn (List.length mfix) f))) mfix in
tCoFix mfix' idx
| x => x
end.
Fixpoint lift n k t : term :=
match t with
| tRel i => tRel (if Nat.leb k i then (n + i) else i)
| tEvar ev args => tEvar ev (List.map (lift n k) args)
| tLambda na T M => tLambda na (lift n k T) (lift n (S k) M)
| tApp u v => tApp (lift n k u) (lift n k v)
| tProd na A B => tProd na (lift n k A) (lift n (S k) B)
| tLetIn na b t b' => tLetIn na (lift n k b) (lift n k t) (lift n (S k) b')
| tCase ind p c brs =>
let brs' := List.map (on_snd (lift n k)) brs in
tCase ind (lift n k p) (lift n k c) brs'
| tProj p c => tProj p (lift n k c)
| tFix mfix idx =>
let k' := List.length mfix + k in
let mfix' := List.map (map_def (lift n k) (lift n k')) mfix in
tFix mfix' idx
| tCoFix mfix idx =>
let k' := List.length mfix + k in
let mfix' := List.map (map_def (lift n k) (lift n k')) mfix in
tCoFix mfix' idx
| x => x
end.
Notation lift0 n := (lift n 0).
Fixpoint subst s k u :=
match u with
| tRel n =>
if Nat.leb k n then
match nth_error s (n - k) with
| Some b => lift0 k b
| None => tRel (n - List.length s)
end
else tRel n
| tEvar ev args => tEvar ev (List.map (subst s k) args)
| tLambda na T M => tLambda na (subst s k T) (subst s (S k) M)
| tApp u v => tApp (subst s k u) (subst s k v)
| tProd na A B => tProd na (subst s k A) (subst s (S k) B)
| tLetIn na b ty b' => tLetIn na (subst s k b) (subst s k ty) (subst s (S k) b')
| tCase ind p c brs =>
let brs' := List.map (on_snd (subst s k)) brs in
tCase ind (subst s k p) (subst s k c) brs'
| tProj p c => tProj p (subst s k c)
| tFix mfix idx =>
let k' := List.length mfix + k in
let mfix' := List.map (map_def (subst s k) (subst s k')) mfix in
tFix mfix' idx
| tCoFix mfix idx =>
let k' := List.length mfix + k in
let mfix' := List.map (map_def (subst s k) (subst s k')) mfix in
tCoFix mfix' idx
| x => x
end.
Inductive assumption_context : context -> Prop :=
| assumption_context_nil : assumption_context []
| assumption_context_vass na t Γ : assumption_context Γ -> assumption_context (vass na t :: Γ).
Fixpoint closedn k (t : term) : bool :=
match t with
| tRel i => Nat.ltb i k
| tEvar ev args => List.forallb (closedn k) args
| tLambda _ T M | tProd _ T M => closedn k T && closedn (S k) M
| tApp u v => closedn k u && closedn k v
| tLetIn na b t b' => closedn k b && closedn k t && closedn (S k) b'
| tCase ind p c brs =>
let brs' := List.forallb (test_snd (closedn k)) brs in
closedn k p && closedn k c && brs'
| tProj p c => closedn k c
| tFix mfix idx =>
let k' := List.length mfix + k in
List.forallb (test_def (closedn k) (closedn k')) mfix
| tCoFix mfix idx =>
let k' := List.length mfix + k in
List.forallb (test_def (closedn k) (closedn k')) mfix
| _ => true
end.
Definition up k (s : nat -> term) :=
fun i =>
if k <=? i then rename (add k) (s (i - k))
else tRel i.
Fixpoint inst s u :=
match u with
| tRel n => s n
| tEvar ev args => tEvar ev (List.map (inst s) args)
| tLambda na T M => tLambda na (inst s T) (inst (up 1 s) M)
| tApp u v => tApp (inst s u) (inst s v)
| tProd na A B => tProd na (inst s A) (inst (up 1 s) B)
| tLetIn na b ty b' => tLetIn na (inst s b) (inst s ty) (inst (up 1 s) b')
| tCase ind p c brs =>
let brs' := List.map (on_snd (inst s)) brs in
tCase ind (inst s p) (inst s c) brs'
| tProj p c => tProj p (inst s c)
| tFix mfix idx =>
let mfix' := map (map_def (inst s) (inst (up (List.length mfix) s))) mfix in
tFix mfix' idx
| tCoFix mfix idx =>
let mfix' := map (map_def (inst s) (inst (up (List.length mfix) s))) mfix in
tCoFix mfix' idx
| x => x
end.
Declare Scope sigma_scope.
Local Open Scope sigma_scope.
Notation "t '.[' σ ]" := (inst σ t) (at level 6, format "t .[ σ ]") : sigma_scope.
Definition subst_compose (σ τ : nat -> term) :=
fun i => (σ i).[τ].
Infix "∘s" := subst_compose (at level 40) : sigma_scope.
Definition ids (x : nat) := tRel x.
Lemma subst_ids t : t.[ids] = t.
admit.
Defined.
Definition shiftk (k : nat) (x : nat) := tRel (k + x).
Notation "↑^ k" := (shiftk k) (at level 30, k at level 2, format "↑^ k") : sigma_scope.
Definition subst_consn {A} (l : list A) (σ : nat -> A) :=
fun i =>
match List.nth_error l i with
| None => σ (i - List.length l)
| Some t => t
end.
Notation " t ⋅n s " := (subst_consn t s) (at level 40) : sigma_scope.
Fixpoint idsn n : list term :=
match n with
| 0 => []
| S n => idsn n ++ [tRel n]
end.
Definition Upn n σ := idsn n ⋅n (σ ∘s ↑^n).
Notation "⇑^ n σ" := (Upn n σ) (at level 30, n at level 2, format "⇑^ n σ") : sigma_scope.
Theorem subst_inst s k t : subst s k t = inst (⇑^k (subst_consn s ids)) t.
admit.
Defined.
Hint Rewrite @subst_inst : sigma.
Import Coq.ssr.ssreflect.
Lemma inst_ext_closed s s' k t :
closedn k t ->
(forall x, x < k -> s x = s' x) ->
inst s t = inst s' t.
admit.
Defined.
Lemma subst_id s Γ t :
closedn #|s| t ->
assumption_context Γ ->
s = List.rev (to_extended_list Γ) ->
subst s 0 t = t.
Proof.
intros cl ass eq.
autorewrite with sigma.
rewrite -{2}(subst_ids t).
eapply inst_ext_closed; eauto.
intros.
unfold ids, subst_consn.
simpl.
destruct (snd (nth_error_Some' s x) H).Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 8.0KiB; full 14KiB file on GitHub Actions Artifacts under
|
1 task
Alizter
force-pushed
the
setoid-rewrite-type
branch
from
4bd2ea0
to
4a7788a
Compare
|
I've rebased and added some bugs that are fixed to the test-suite. |
Alizter
added
part: rewriting tactics
|
I don't think we need to update any documentation about this. AFAIK CMorphism ("computational" morphism btw) is not documented anywhere. It doesn't make sense to introduce it here either since this is a bug fix. Though it could also be argued that this is the "official" introduction of the polymorphic generalized rewriting in which case some documentation should be written. I'm going to mark this as ready for review since I would like to see these bugs fixed soon. |
|
Hey, I have detected that there were CI failures at commit a771fd3 without any failure in the test-suite. |
1 similar comment
|
Hey, I have detected that there were CI failures at commit a771fd3 without any failure in the test-suite. |
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
|
@JasonGross No need to minimize category_theory since it is just renaming a few things and getting rid of a Fail. I am currently preparing the overlay for that. I haven't yet worked out what metacoq is doing yet. |
Alizter
added
the
needs: overlay
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
Alizter
added
kind: fix
SkySkimmer
reviewed
Jan 5, 2022
SkySkimmer
approved these changes
Jan 5, 2022
SkySkimmer
reviewed
Jan 5, 2022
Alizter
force-pushed
the
setoid-rewrite-type
branch
from
5245db3
to
0d994fc
Compare
Author: Matthieu Sozeau <mattam@mattam.org> Date: Tue Apr 20 11:40:50 2021 +0200 Please enter the commit message for your changes. Lines starting
Author: Matthieu Sozeau <mattam@mattam.org> Date: Tue Apr 20 11:40:50 2021 +0200
Alizter
force-pushed
the
setoid-rewrite-type
branch
from
0d994fc
to
28455c0
Compare
ppedrot
added a commit
to MetaCoq/metacoq
that referenced
this pull request
Jan 7, 2022
|
|
@SkySkimmer Would you say that is just noise? |
|
No, that's not noise. |
|
@SkySkimmer Are we ready to merge? |
|
Waiting for the overlay |
|
I checked corn and there doesn't appear to be any big slow downs, just a lot of smaller ones. |
|
@SkySkimmer Overlays have been merged. |
|
@coqbot merge now |
|
@SkySkimmer: Please take care of the following overlays:
|
|
Test suite and bedrock broke in master, not sure why so I made a revert PR #15476 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We were missing a few universe refreshings in the ML code resulting in unsatisfiable constraints. We add a test ensuring that indeed setoid_rewrite works with (monomorphic) relations in Type and in the universe polymorphic mode as well.
Certainly fixes a number of bugs, I'll gather them.
Kind: bug fix / feature
https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md for details)