Merge branch 'main' into ext/prop-eq

scripts/generate_dep.py

@@ -1,4 +1,4 @@
-import re, sys, textwrap
+import itertools, re, sys, textwrap
 from pathlib import Path
 from typing import Iterable
 
@@ -48,8 +48,9 @@ def module_name_of_path(path: str) -> str:
 
 def node_of_path(path: str) -> str:
     parts = module_parts_of_path(path)
-    color = next((COLORS[parts[i]] for i in range(len(parts)-1,-1,-1) if parts[i] in COLORS),COLORS["others"])
-    subgraph_names = ["/".join(parts[:partindex]) for partindex in range(1,len(parts))]
+    dedupe_parts = list(dict.fromkeys(parts))
+    color = next((COLORS[part] for part in reversed(dedupe_parts) if part in COLORS),COLORS["others"])
+    subgraph_names = list(itertools.accumulate(parts[:-1], func="{0}/{1}".format))
     module_name = module_name_of_module_parts(parts)
     node_label = parts[-1]
 
@@ -59,6 +60,8 @@ def node_of_path(path: str) -> str:
         result = under_subgraph(f"Core/{node_label}", f""""{module_name}"[label="{node_label}",tooltip="{module_name}",color={color},fillcolor=white];""")
     elif module_name == "Mcltt.LibTactics":
         result = f"""{{ graph[cluster=false,rank=min]; "{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}]; }}"""
+    elif module_name == "Mcltt.Core.Semantic.Consequences":
+        result = f"""{{ cluster=false; rank=max; "{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}]; }}"""
     else:
         result = f""""{module_name}"[label="{node_label}",tooltip="{module_name}",fillcolor={color}];"""
 

theories/Algorithmic/Subtyping.v

@@ -0,0 +1 @@
+From Mcltt.Algorithmic.Subtyping Require Export Definitions Lemmas.

theories/Algorithmic/Subtyping/Definitions.v

@@ -1,6 +1,6 @@
-From Mcltt Require Import Base.
-From Mcltt.Core Require Import System.Definitions NbE.
-From Mcltt Require Export Syntax.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Export NbE.
+From Mcltt.Core.Syntactic Require Export SystemOpt.
 Import Syntax_Notations.
 
 Reserved Notation "Γ ⊢a A ⊆ A'" (in custom judg at level 80, Γ custom exp, A custom exp, A' custom exp).

theories/Algorithmic/Subtyping/Lemmas.v

@@ -1,8 +1,8 @@
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation Readback NbE CoreTypeInversions Presup CtxSub SystemOpt.
-From Mcltt.Core.Completeness Require Import Consequences.Rules.
-From Mcltt Require Import Completeness Soundness.
-From Mcltt.Algorithmic Require Import Subtyping.Definitions.
+From Mcltt Require Import LibTactics.
+From Mcltt.Algorithmic.Subtyping Require Import Definitions.
+From Mcltt.Core Require Import Base Soundness.
+From Mcltt.Core.Syntactic Require Import SystemOpt.
+From Mcltt.Core.Completeness.Consequences Require Import Rules.
 Import Syntax_Notations.
 
 #[local]

theories/Algorithmic/Typing.v

@@ -0,0 +1 @@
+From Mcltt.Algorithmic.Typing Require Export Definitions Lemmas.

theories/Algorithmic/Typing/Definitions.v

@@ -1,9 +1,5 @@
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Algorithmic Require Export Subtyping.Definitions.
-From Mcltt.Core Require Import Soundness Completeness.
-From Mcltt.Core.Semantic Require Import NbE.
-From Mcltt.Core.Syntactic Require Import System.Definitions.
-From Mcltt.Core.Syntactic Require Export Syntax.
+From Mcltt.Algorithmic.Subtyping Require Export Definitions.
+From Mcltt.Core Require Import Base.
 Import Domain_Notations.
 
 Reserved Notation "Γ '⊢a' M ⟹ A" (in custom judg at level 80, Γ custom exp, M custom exp, A custom nf).

theories/Algorithmic/Typing/Lemmas.v

@@ -1,10 +1,9 @@
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Algorithmic Require Import Typing.Definitions.
-From Mcltt.Algorithmic Require Export Subtyping.Lemmas.
-From Mcltt.Core Require Import Soundness Completeness.
+From Mcltt Require Import LibTactics.
+From Mcltt.Algorithmic.Typing Require Import Definitions.
+From Mcltt.Algorithmic.Subtyping Require Export Lemmas.
+From Mcltt.Core Require Import Base.
 From Mcltt.Core.Completeness Require Import Consequences.Rules.
 From Mcltt.Core.Semantic Require Import Consequences.
-From Mcltt.Core.Syntactic Require Export SystemOpt.
 From Mcltt.Frontend Require Import Elaborator.
 Import Domain_Notations.
 

theories/Core/Completeness.v

@@ -1,5 +1,6 @@
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core.Completeness Require Import FundamentalTheorem.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Completeness Require Export FundamentalTheorem.
 From Mcltt.Core.Semantic Require Import Realizability.
 From Mcltt.Core.Semantic Require Export NbE.
 From Mcltt.Core.Syntactic Require Export SystemOpt.

theories/Core/Completeness/Consequences/Rules.v

@@ -1,7 +1,8 @@
 From Coq Require Import RelationClasses.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness Completeness.FundamentalTheorem Completeness.LogicalRelation Semantic.Realizability PER.
-From Mcltt.Core Require Export SystemOpt.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core Require Export Completeness.
+From Mcltt.Core.Semantic Require Import Realizability.
 Import Domain_Notations.
 
 Lemma ctxeq_nbe_eq : forall Γ Γ' M A,

theories/Core/Completeness/Consequences/Types.v

@@ -1,7 +1,8 @@
 From Coq Require Import RelationClasses.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness Completeness.FundamentalTheorem Completeness.LogicalRelation Semantic.Realizability.
-From Mcltt.Core Require Export SystemOpt.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core Require Export Completeness.
+From Mcltt.Core.Semantic Require Import Realizability.
 Import Domain_Notations.
 
 Lemma exp_eq_typ_implies_eq_level : forall {Γ i j k},

theories/Core/Completeness/ContextCases.v

@@ -1,6 +1,7 @@
 From Coq Require Import Morphisms_Relations.
 
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
 From Mcltt.Core.Completeness Require Import LogicalRelation UniverseCases.
 Import Domain_Notations.
 

theories/Core/Completeness/FunctionCases.v

@@ -1,6 +1,7 @@
 From Coq Require Import Morphisms_Relations Relation_Definitions.
 
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
 From Mcltt.Core.Completeness Require Import LogicalRelation TermStructureCases UniverseCases.
 Import Domain_Notations.
 

theories/Core/Completeness/LogicalRelation.v

@@ -1 +1 @@
-From Mcltt.Core.Completeness Require Export LogicalRelation.Definitions LogicalRelation.Lemmas LogicalRelation.Tactics.
+From Mcltt.Core.Completeness.LogicalRelation Require Export Definitions Lemmas Tactics.

theories/Core/Completeness/LogicalRelation/Definitions.v

@@ -1,6 +1,6 @@
 From Coq Require Import Relations.
-From Mcltt Require Import Base.
-From Mcltt.Core Require Export PER.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Export PER.
 Import Domain_Notations.
 
 Inductive rel_exp M ρ M' ρ' (R : relation domain) : Prop :=

theories/Core/Completeness/LogicalRelation/Lemmas.v

@@ -1,6 +1,8 @@
 From Coq Require Import Morphisms Morphisms_Relations RelationClasses Relation_Definitions.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core.Completeness Require Import LogicalRelation.Definitions LogicalRelation.Tactics.
+
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Completeness.LogicalRelation Require Import Definitions Tactics.
 Import Domain_Notations.
 
 Add Parametric Morphism M ρ M' ρ' : (rel_exp M ρ M' ρ')

theories/Core/Completeness/LogicalRelation/Tactics.v

@@ -1,5 +1,6 @@
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import PER.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Import PER.
 Import Domain_Notations.
 
 Ltac eexists_rel_exp :=

theories/Core/Completeness/NatCases.v

@@ -1,6 +1,7 @@
 From Coq Require Import Morphisms_Relations.
 
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
 From Mcltt.Core.Completeness Require Import LogicalRelation SubstitutionCases TermStructureCases UniverseCases.
 From Mcltt.Core.Semantic Require Import Realizability.
 Import Domain_Notations.

theories/Core/Completeness/SubstitutionCases.v

@@ -1,6 +1,7 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
 From Mcltt.Core.Completeness Require Import ContextCases LogicalRelation UniverseCases.
 Import Domain_Notations.
 

theories/Core/Completeness/SubtypingCases.v

@@ -1,6 +1,7 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
 From Mcltt.Core.Completeness Require Import LogicalRelation FunctionCases.
 Import Domain_Notations.
 

theories/Core/Completeness/TermStructureCases.v

@@ -1,6 +1,7 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
 From Mcltt.Core.Completeness Require Import LogicalRelation UniverseCases.
 Import Domain_Notations.
 

theories/Core/Completeness/UniverseCases.v

@@ -1,6 +1,7 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
 
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
 From Mcltt.Core.Completeness Require Import LogicalRelation.
 Import Domain_Notations.
 

theories/Core/Completeness/VariableCases.v

@@ -1,6 +1,7 @@
 From Coq Require Import Morphisms_Relations.
 
-From Mcltt Require Import Base LibTactics.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
 From Mcltt.Core.Completeness Require Import LogicalRelation.
 From Mcltt.Core.Syntactic Require Import SystemOpt.
 Import Domain_Notations.

theories/Core/Semantic/Consequences.v

@@ -1,8 +1,7 @@
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Completeness Soundness.
-From Mcltt.Core.Completeness Require Import Consequences.Types LogicalRelation.
-From Mcltt.Core.Semantic Require Import NbE.
-From Mcltt.Core.Syntactic Require Export SystemOpt.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core Require Export Soundness.
+From Mcltt.Core.Completeness.Consequences Require Export Types.
 Import Domain_Notations.
 
 Lemma adjust_exp_eq_level : forall {Γ A A' i j},

theories/Core/Semantic/Domain.v

@@ -1,6 +1,7 @@
-From Mcltt Require Export Syntax.
 From Equations Require Import Equations.
 
+From Mcltt.Core.Syntactic Require Export Syntax.
+
 Reserved Notation "'env'".
 
 Inductive domain : Set :=

theories/Core/Semantic/Evaluation.v

@@ -1 +1 @@
-From Mcltt Require Export Evaluation.Definitions Evaluation.Lemmas Evaluation.Tactics.
+From Mcltt.Core.Semantic.Evaluation Require Export Definitions Lemmas Tactics.

theories/Core/Semantic/Evaluation/Definitions.v

@@ -1,5 +1,5 @@
-From Mcltt Require Import Base.
-From Mcltt Require Export Domain.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Export Domain.
 Import Domain_Notations.
 
 Reserved Notation "'⟦' M '⟧' ρ '↘' r" (in custom judg at level 80, M custom exp at level 99, ρ custom domain at level 99, r custom domain at level 99).

theories/Core/Semantic/Evaluation/Lemmas.v

@@ -1,5 +1,8 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base LibTactics Evaluation.Definitions.
+
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic.Evaluation Require Import Definitions.
 Import Domain_Notations.
 
 Section functional_eval.

theories/Core/Semantic/Evaluation/Tactics.v

@@ -1,4 +1,6 @@
-From Mcltt Require Import Base LibTactics Evaluation.Definitions Evaluation.Lemmas.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic.Evaluation Require Import Definitions Lemmas.
 Import Domain_Notations.
 
 Ltac simplify_evals :=

theories/Core/Semantic/NbE.v

@@ -1,5 +1,6 @@
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Export Domain Evaluation Readback.
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Export Domain Evaluation Readback.
 Import Domain_Notations.
 
 Generalizable All Variables.

theories/Core/Semantic/PER.v

@@ -1 +1 @@
-From Mcltt Require Export PER.Definitions PER.Lemmas PER.CoreTactics.
+From Mcltt.Core.Semantic.PER Require Export CoreTactics Definitions Lemmas.

theories/Core/Semantic/PER/CoreTactics.v

@@ -1,7 +1,9 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import PER.Definitions.
+
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Import PER.Definitions.
 Import Domain_Notations.
 
 Ltac destruct_rel_by_assumption in_rel H :=

theories/Core/Semantic/PER/Definitions.v

@@ -1,7 +1,9 @@
 From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Export Domain Evaluation Readback.
+
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Export Domain Evaluation Readback.
 Import Domain_Notations.
 
 Notation "'Dom' a ≈ b ∈ R" := ((R a b : Prop) : Prop) (in custom judg at level 90, a custom domain, b custom domain, R constr).

theories/Core/Semantic/PER/Lemmas.v

@@ -1,7 +1,9 @@
 From Coq Require Import Equivalence Lia Morphisms Morphisms_Prop Morphisms_Relations PeanoNat Relation_Definitions RelationClasses.
 From Equations Require Import Equations.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import PER.Definitions PER.CoreTactics.
+
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Import PER.CoreTactics PER.Definitions.
 Import Domain_Notations.
 
 Add Parametric Morphism R0 `(R0_morphism : Proper _ ((@relation_equivalence domain) ==> (@relation_equivalence domain)) R0) A ρ A' ρ' : (rel_mod_eval R0 A ρ A' ρ')

theories/Core/Semantic/Readback.v

@@ -1 +1 @@
-From Mcltt Require Export Readback.Definitions Readback.Lemmas.
+From Mcltt.Core.Semantic.Readback Require Export Definitions Lemmas.

theories/Core/Semantic/Readback/Definitions.v

@@ -1,5 +1,6 @@
-From Mcltt.Core Require Import Base Evaluation.
-From Mcltt Require Export Domain.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Import Evaluation.
+From Mcltt.Core.Semantic Require Export Domain.
 Import Domain_Notations.
 
 Reserved Notation "'Rnf' m 'in' s ↘ M" (in custom judg at level 80, m custom domain, s constr, M custom nf).

theories/Core/Semantic/Readback/Lemmas.v

@@ -1,6 +1,9 @@
 From Coq Require Import Lia PeanoNat Relations.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation Readback.Definitions.
+
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Import Evaluation.
+From Mcltt.Core.Semantic.Readback Require Import Definitions.
 Import Domain_Notations.
 
 Section functional_read.

theories/Core/Semantic/Realizability.v

@@ -1,7 +1,9 @@
 From Coq Require Import Lia Morphisms_Relations PeanoNat Relation_Definitions.
 From Equations Require Import Equations.
-From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Export NbE PER.
+
+From Mcltt Require Import LibTactics.
+From Mcltt.Core Require Import Base.
+From Mcltt.Core.Semantic Require Export NbE PER.
 Import Domain_Notations.
 
 Lemma per_nat_then_per_top : forall {n m},