diff --git a/.github/workflows/ci_build.yaml b/.github/workflows/ci_build.yaml index 227123e..3534de6 100644 --- a/.github/workflows/ci_build.yaml +++ b/.github/workflows/ci_build.yaml @@ -30,7 +30,7 @@ jobs: contents: write env: REGISTRY: "ghcr.io" - IMAGE_TAG: "beluga-lang/mcltt:main" + IMAGE_TAG: "beluga-lang/mctt:main" # Only deploy if the build follows from pushing to one of main branches DOC_DEPLOY: ${{ (github.ref_name == 'main' || startsWith(github.ref_name, 'ext/')) && 'true' || 'false' }} DOC_DEPLOY_DEST: ${{ startsWith(github.ref_name, 'ext/') && github.ref_name || '' }} @@ -73,8 +73,8 @@ jobs: mv theories/dep.html html/dep.html cp assets/styling.css html/styling.css cp -r assets/images html/images - sed -i 's!\[Coqdoc\](https://beluga-lang\.github\.io/McLTT/dep\.html)![Coqdoc](dep.html)!' README.md - pandoc README.md -H assets/include.html --no-highlight --metadata pagetitle='McLTT: A Bottom-up Approach to Implementing A Proof Assistant' -t html --css styling.css -o html/index.html + sed -i 's!\[Coqdoc\](https://beluga-lang\.github\.io/McTT/dep\.html)![Coqdoc](dep.html)!' README.md + pandoc README.md -H assets/include.html --no-highlight --metadata pagetitle='McTT: Building A Correct-By-Construction Proof Checkers For Type Theories' -t html --css styling.css -o html/index.html fi endGroup startGroup "Run inline tests" diff --git a/README.md b/README.md index 60fb845..cf1c0e3 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,8 @@ -# McLTT: A Bottom-up Approach to Implementing A Proof Assistant +# McTT: Building A Correct-By-Construction Proof Checkers For Type Theories -McLTT is a verified, runnable typechecker for Martin-Löf type theory. This project provides an executable, to which we can feed +McTT is a verified, runnable typechecker for Martin-Löf type theory. This project provides an executable, to which we can feed a program in Martin-Löf type theory to check whether this -program has the specified type. McLTT is novel in that it is implemented and verified in +program has the specified type. McTT is novel in that it is implemented and verified in Coq. More specifically, we proved that the typechecking algorithm extracted from Coq is sound and complete: a program passes typechecker if and only if it is a well-typed program in MLTT. This is the first verified proof assistant (despite being @@ -10,14 +10,14 @@ elementary) and serves as a basis for future extensions. ## Online Documentation -We have generated a [Coqdoc](https://beluga-lang.github.io/McLTT/dep.html) for browsing our Coq proof. +We have generated a [Coqdoc](https://beluga-lang.github.io/McTT/dep.html) for browsing our Coq proof. ## Architecture -McLTT has the following architecture: +McTT has the following architecture: ``` - | source code of McLTT + | source code of McTT v +-------+ | lexer | OCaml code generated by ocamllex @@ -58,6 +58,7 @@ implementation. We recommend to install dependencies in the following way: ```bash +opam update opam switch create coq-8.20.0 4.14.2 opam pin add coq 8.20.0 opam repo add coq-released https://coq.inria.fr/opam/released @@ -75,11 +76,11 @@ possible. Once `make` finishes, you can run the binary: ``` -dune exec mcltt examples/nary.mcl # or your own example +dune exec mctt examples/nary.mctt # or your own example ``` or more directly ``` -_build/default/driver/mcltt.exe examples/nary.mcl # or your own example +_build/default/driver/mctt.exe examples/nary.mctt # or your own example ``` To build Coq proof only, you can go into and only build the `theories` directory: diff --git a/assets/include.html b/assets/include.html index abc4cba..4396009 100644 --- a/assets/include.html +++ b/assets/include.html @@ -16,7 +16,7 @@ var header = $(`
- Fork on GitHub + Fork on GitHub ${h1elem.outerHTML}
`); diff --git a/driver/Lexer.mli b/driver/Lexer.mli index c3a2e91..ec6a6c3 100644 --- a/driver/Lexer.mli +++ b/driver/Lexer.mli @@ -1,7 +1,7 @@ val format_position : Format.formatter -> Lexing.position -> unit val format_range : Format.formatter -> Lexing.position * Lexing.position -> unit -val format_token : Format.formatter -> MclttExtracted.Parser.token -> unit -val read : Lexing.lexbuf -> MclttExtracted.Parser.token +val format_token : Format.formatter -> McttExtracted.Parser.token -> unit +val read : Lexing.lexbuf -> McttExtracted.Parser.token val lexbuf_to_token_buffer : - Lexing.lexbuf -> MclttExtracted.Parser.MenhirLibParser.Inter.buffer + Lexing.lexbuf -> McttExtracted.Parser.MenhirLibParser.Inter.buffer diff --git a/driver/Lexer.mll b/driver/Lexer.mll index c74eddd..fee5c9d 100644 --- a/driver/Lexer.mll +++ b/driver/Lexer.mll @@ -1,6 +1,6 @@ { open Lexing - open MclttExtracted.Parser + open McttExtracted.Parser let get_range lexbuf = (lexbuf.lex_start_p, lexbuf.lex_curr_p) diff --git a/driver/Main.ml b/driver/Main.ml index 63a84d7..e2b66c3 100644 --- a/driver/Main.ml +++ b/driver/Main.ml @@ -1,5 +1,5 @@ -module Parser = MclttExtracted.Parser -module Entrypoint = MclttExtracted.Entrypoint +module Parser = McttExtracted.Parser +module Entrypoint = McttExtracted.Entrypoint open Parser open MenhirLibParser.Inter open Entrypoint diff --git a/driver/Mcltt.ml b/driver/Mctt.ml similarity index 94% rename from driver/Mcltt.ml rename to driver/Mctt.ml index 29ca6d2..fb43d2e 100644 --- a/driver/Mcltt.ml +++ b/driver/Mctt.ml @@ -1,4 +1,4 @@ -open Mcltt.Main +open Mctt.Main let () = if Array.length Sys.argv <> 2 diff --git a/driver/PrettyPrinter.ml b/driver/PrettyPrinter.ml index a499862..80f2a09 100644 --- a/driver/PrettyPrinter.ml +++ b/driver/PrettyPrinter.ml @@ -1,7 +1,7 @@ -open MclttExtracted.Entrypoint -open MclttExtracted.Syntax -module Parser = MclttExtracted.Parser -module ParserMessages = MclttExtracted.ParserMessages +open McttExtracted.Entrypoint +open McttExtracted.Syntax +module Parser = McttExtracted.Parser +module ParserMessages = McttExtracted.ParserMessages (************************************************************) (* Formatting helpers *) diff --git a/driver/PrettyPrinter.mli b/driver/PrettyPrinter.mli index 0ceb66b..bc56ee1 100644 --- a/driver/PrettyPrinter.mli +++ b/driver/PrettyPrinter.mli @@ -1,6 +1,6 @@ -val format_obj : Format.formatter -> MclttExtracted.Syntax.Cst.obj -> unit -val format_exp : Format.formatter -> MclttExtracted.Syntax.exp -> unit -val format_nf : Format.formatter -> MclttExtracted.Syntax.nf -> unit +val format_obj : Format.formatter -> McttExtracted.Syntax.Cst.obj -> unit +val format_exp : Format.formatter -> McttExtracted.Syntax.exp -> unit +val format_nf : Format.formatter -> McttExtracted.Syntax.nf -> unit val format_main_result : - Format.formatter -> MclttExtracted.Entrypoint.main_result -> unit + Format.formatter -> McttExtracted.Entrypoint.main_result -> unit diff --git a/driver/Test.ml b/driver/Test.ml index 0c156c5..c8ce29e 100644 --- a/driver/Test.ml +++ b/driver/Test.ml @@ -1,7 +1,7 @@ (* Unit test cases for parsing *) open Main -open MclttExtracted.Entrypoint +open McttExtracted.Entrypoint (** Helper definitions *) @@ -100,8 +100,8 @@ let%expect_test "recursion on a natural number that always returns zero is of \ 0 : Nat |}] -let%expect_test "simple_nat.mcl works" = - let _ = main_of_example "simple_nat.mcl" in +let%expect_test "simple_nat.mctt works" = + let _ = main_of_example "simple_nat.mctt" in [%expect {| Parsed: @@ -112,8 +112,8 @@ let%expect_test "simple_nat.mcl works" = 4 : Nat |}] -let%expect_test "simple_rec.mcl works" = - let _ = main_of_example "simple_rec.mcl" in +let%expect_test "simple_rec.mctt works" = + let _ = main_of_example "simple_rec.mctt" in [%expect {| Parsed: @@ -129,8 +129,8 @@ let%expect_test "simple_rec.mcl works" = : forall (x1 : Nat) -> Nat |}] -let%expect_test "pair.mcl works" = - let _ = main_of_example "pair.mcl" in +let%expect_test "pair.mctt works" = + let _ = main_of_example "pair.mctt" in [%expect {| Parsed: @@ -255,8 +255,8 @@ let%expect_test "pair.mcl works" = 5 : Nat |}] -let%expect_test "vector.mcl works" = - let _ = main_of_example "vector.mcl" in +let%expect_test "vector.mctt works" = + let _ = main_of_example "vector.mctt" in [%expect {| Parsed: @@ -463,8 +463,8 @@ let%expect_test "vector.mcl works" = 7 : Nat |}] -let%expect_test "nary.mcl works" = - let _ = main_of_example "nary.mcl" in +let%expect_test "nary.mctt works" = + let _ = main_of_example "nary.mctt" in [%expect {| Parsed: @@ -553,8 +553,8 @@ let%expect_test "nary.mcl works" = 6 : Nat |}] -let%expect_test "simple_let.mcl works" = - let _ = main_of_example "simple_let.mcl" in +let%expect_test "simple_let.mctt works" = + let _ = main_of_example "simple_let.mctt" in [%expect {| Parsed: @@ -565,8 +565,8 @@ let%expect_test "simple_let.mcl works" = 1 : Nat |}] -let%expect_test "let_two_vars.mcl works" = - let _ = main_of_example "let_two_vars.mcl" in +let%expect_test "let_two_vars.mctt works" = + let _ = main_of_example "let_two_vars.mctt" in [%expect {| Parsed: @@ -584,8 +584,8 @@ let%expect_test "let_two_vars.mcl works" = 0 : Nat |}] -let%expect_test "let_nary.mcl works" = - let _ = main_of_example "let_nary.mcl" in +let%expect_test "let_nary.mctt works" = + let _ = main_of_example "let_nary.mctt" in [%expect {| Parsed: @@ -675,8 +675,8 @@ let%expect_test "let_nary.mcl works" = |}] -let%expect_test "let_vector.mcl works" = - let _ = main_of_example "let_vector.mcl" in +let%expect_test "let_vector.mctt works" = + let _ = main_of_example "let_vector.mctt" in [%expect {| Parsed: diff --git a/driver/dune b/driver/dune index 40e0c90..338a5e6 100644 --- a/driver/dune +++ b/driver/dune @@ -1,21 +1,21 @@ (include_subdirs no) (library - (name Mcltt) - (public_name mcltt.driver) + (name Mctt) + (public_name mctt.driver) (modules Main Lexer PrettyPrinter Test) - (libraries MclttExtracted) + (libraries McttExtracted) (inline_tests (deps - (glob_files_rec ../examples/*.mcl))) + (glob_files_rec ../examples/*.mctt))) (preprocess (pps ppx_expect))) (executable - (name mcltt) - (public_name mcltt) - (modules Mcltt) - (libraries Mcltt)) + (name mctt) + (public_name mctt) + (modules Mctt) + (libraries Mctt)) (env (dev diff --git a/driver/extracted/dune b/driver/extracted/dune index aa468c5..4ca696a 100644 --- a/driver/extracted/dune +++ b/driver/extracted/dune @@ -1,5 +1,5 @@ (library - (name MclttExtracted) - (public_name mcltt.extracted)) + (name McttExtracted) + (public_name mctt.extracted)) (documentation) diff --git a/dune-project b/dune-project index e141f18..4cbe9c9 100644 --- a/dune-project +++ b/dune-project @@ -1,6 +1,6 @@ (lang dune 3.13) (using menhir 2.1) -(name mcltt) +(name mctt) (generate_opam_files) @@ -9,20 +9,20 @@ "Jason Hu" "Junyoung Jang") (maintainers "the CompLogic group, McGill University") -(homepage "https://beluga-lang.github.io/McLTT/") -(documentation "https://beluga-lang.github.io/McLTT/") -(source (github Beluga-lang/McLTT)) +(homepage "https://beluga-lang.github.io/McTT/") +(documentation "https://beluga-lang.github.io/McTT/") +(source (github Beluga-lang/McTT)) (package - (name mcltt) - (synopsis "A Bottom-up Approach to Implementing A Proof Assistant") - (description "In McLTT, we build a verified, runnable typechecker for Martin-Löf type theory. After -the accomplishment of this project, we will obtain an executable, to which we can feed -a program in Martin-Loef type theory, and this executable will check whether this -program has the specified type. McLTT is novel in that it is implemented in -Coq. Moreover, we will prove that the typechecking algorithm extracted from Coq is -sound and complete: a program passes typechecking if and only if it is a well-typed -program in MLTT. This will be the first verified proof assistant (despite being + (name mctt) + (synopsis "A Correct-By-Construction Proof Checkers For Type Theories") + (description "McTT is a verified, runnable typechecker for Martin-Löf type +theory. This project provides an executable, to which we can feed a program +in Martin-Löf type theory to check whether this program has the specified type. +McTT is novel in that it is implemented and verified in Coq. More specifically, +we proved that the typechecking algorithm extracted from Coq is sound and +complete: a program passes typechecker if and only if it is a well-typed +program in MLTT. This is the first verified proof assistant (despite being elementary) and serves as a basis for future extensions.") (depends (ocaml (>= "4.14.2")) diff --git a/examples/let_nary.mcl b/examples/let_nary.mctt similarity index 100% rename from examples/let_nary.mcl rename to examples/let_nary.mctt diff --git a/examples/let_two_vars.mcl b/examples/let_two_vars.mctt similarity index 100% rename from examples/let_two_vars.mcl rename to examples/let_two_vars.mctt diff --git a/examples/let_vector.mcl b/examples/let_vector.mctt similarity index 100% rename from examples/let_vector.mcl rename to examples/let_vector.mctt diff --git a/examples/nary.mcl b/examples/nary.mctt similarity index 100% rename from examples/nary.mcl rename to examples/nary.mctt diff --git a/examples/pair.mcl b/examples/pair.mctt similarity index 100% rename from examples/pair.mcl rename to examples/pair.mctt diff --git a/examples/simple_let.mcl b/examples/simple_let.mctt similarity index 100% rename from examples/simple_let.mcl rename to examples/simple_let.mctt diff --git a/examples/simple_nat.mcl b/examples/simple_nat.mctt similarity index 100% rename from examples/simple_nat.mcl rename to examples/simple_nat.mctt diff --git a/examples/simple_rec.mcl b/examples/simple_rec.mctt similarity index 100% rename from examples/simple_rec.mcl rename to examples/simple_rec.mctt diff --git a/examples/vector.mcl b/examples/vector.mctt similarity index 100% rename from examples/vector.mcl rename to examples/vector.mctt diff --git a/mcltt.opam.template b/mctt.opam.template similarity index 100% rename from mcltt.opam.template rename to mctt.opam.template diff --git a/scripts/generate_dep.py b/scripts/generate_dep.py index 56fc515..c3840ca 100644 --- a/scripts/generate_dep.py +++ b/scripts/generate_dep.py @@ -4,7 +4,7 @@ PROJECT_ROOT = Path(__file__).resolve().parents[1] THEORIES_ROOT = PROJECT_ROOT / "theories" -ROOT_MODULE_NAME = "Mcltt" +ROOT_MODULE_NAME = "Mctt" COLORS = { "Algorithmic": "darkturquoise", "Completeness": "deeppink3", @@ -57,11 +57,11 @@ def node_of_path(path: str) -> str: # Handle special case for two main theorems # so that printed graph looks better - if module_name == "Mcltt.Core.Completeness" or module_name == "Mcltt.Core.Soundness": + if module_name == "Mctt.Core.Completeness" or module_name == "Mctt.Core.Soundness": 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": + elif module_name == "Mctt.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": + elif module_name == "Mctt.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}];""" @@ -92,9 +92,9 @@ def data_of_depline(depline: str) -> str: def gen_graph() -> str: newline = "\n" return textwrap.dedent(f""" - digraph Mcltt {{ - graph [center=true,class="depgraph",cluster=true,fontname="Open Sans",fontsize=28,label="Mcltt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""]; - node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McLTT/{DOC_BASE}/\\N.html"]; + digraph Mctt {{ + graph [center=true,class="depgraph",cluster=true,fontname="Open Sans",fontsize=28,label="Mctt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""]; + node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McTT/{DOC_BASE}/\\N.html"]; {default_subgraph_decl("Algorithmic")} {default_subgraph_decl("Core")} {core_subgraph_decl("Completeness")} diff --git a/theories/Algorithmic/Subtyping.v b/theories/Algorithmic/Subtyping.v index ca21f2d..5795de9 100644 --- a/theories/Algorithmic/Subtyping.v +++ b/theories/Algorithmic/Subtyping.v @@ -1 +1 @@ -From Mcltt.Algorithmic.Subtyping Require Export Definitions Lemmas. +From Mctt.Algorithmic.Subtyping Require Export Definitions Lemmas. diff --git a/theories/Algorithmic/Subtyping/Definitions.v b/theories/Algorithmic/Subtyping/Definitions.v index b06001c..7927305 100644 --- a/theories/Algorithmic/Subtyping/Definitions.v +++ b/theories/Algorithmic/Subtyping/Definitions.v @@ -1,6 +1,6 @@ -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Export NbE. -From Mcltt.Core.Syntactic Require Export SystemOpt. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Export NbE. +From Mctt.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). @@ -35,4 +35,4 @@ Inductive alg_subtyping : ctx -> typ -> typ -> Prop := where "Γ ⊢a A ⊆ B" := (alg_subtyping Γ A B) (in custom judg) : type_scope. #[export] -Hint Constructors alg_subtyping_nf alg_subtyping: mcltt. +Hint Constructors alg_subtyping_nf alg_subtyping: mctt. diff --git a/theories/Algorithmic/Subtyping/Lemmas.v b/theories/Algorithmic/Subtyping/Lemmas.v index 18e3d17..b91c626 100644 --- a/theories/Algorithmic/Subtyping/Lemmas.v +++ b/theories/Algorithmic/Subtyping/Lemmas.v @@ -1,8 +1,8 @@ -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. +From Mctt Require Import LibTactics. +From Mctt.Algorithmic.Subtyping Require Import Definitions. +From Mctt.Core Require Import Base Soundness. +From Mctt.Core.Syntactic Require Import SystemOpt. +From Mctt.Core.Completeness.Consequences Require Import Rules. Import Syntax_Notations. #[local] @@ -61,7 +61,7 @@ Proof. Qed. #[local] -Hint Resolve alg_subtyping_nf_trans alg_subtyping_nf_refl : mcltt. +Hint Resolve alg_subtyping_nf_trans alg_subtyping_nf_refl : mctt. Lemma alg_subtyping_trans : forall Γ A0 A1 A2, {{ Γ ⊢a A0 ⊆ A1 }} -> @@ -74,7 +74,7 @@ Proof. Qed. #[local] -Hint Resolve alg_subtyping_trans : mcltt. +Hint Resolve alg_subtyping_trans : mctt. Lemma alg_subtyping_complete : forall Γ A B, {{ Γ ⊢ A ⊆ B }} -> diff --git a/theories/Algorithmic/Typing.v b/theories/Algorithmic/Typing.v index 365afcd..3e3eb8d 100644 --- a/theories/Algorithmic/Typing.v +++ b/theories/Algorithmic/Typing.v @@ -1 +1 @@ -From Mcltt.Algorithmic.Typing Require Export Definitions Lemmas. +From Mctt.Algorithmic.Typing Require Export Definitions Lemmas. diff --git a/theories/Algorithmic/Typing/Definitions.v b/theories/Algorithmic/Typing/Definitions.v index 010eab6..ba74899 100644 --- a/theories/Algorithmic/Typing/Definitions.v +++ b/theories/Algorithmic/Typing/Definitions.v @@ -1,5 +1,5 @@ -From Mcltt.Algorithmic.Subtyping Require Export Definitions. -From Mcltt.Core Require Import Base. +From Mctt.Algorithmic.Subtyping Require Export Definitions. +From Mctt.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). @@ -51,7 +51,7 @@ with alg_type_infer : ctx -> nf -> exp -> Prop := where "Γ '⊢a' M ⟹ A" := (alg_type_infer Γ A M) (in custom judg) : type_scope. #[export] -Hint Constructors alg_type_check alg_type_infer : mcltt. +Hint Constructors alg_type_check alg_type_infer : mctt. Scheme alg_type_check_mut_ind := Induction for alg_type_check Sort Prop with alg_type_infer_mut_ind := Induction for alg_type_infer Sort Prop. diff --git a/theories/Algorithmic/Typing/Lemmas.v b/theories/Algorithmic/Typing/Lemmas.v index ebe95ab..e063ba9 100644 --- a/theories/Algorithmic/Typing/Lemmas.v +++ b/theories/Algorithmic/Typing/Lemmas.v @@ -1,10 +1,10 @@ -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.Frontend Require Import Elaborator. +From Mctt Require Import LibTactics. +From Mctt.Algorithmic.Typing Require Import Definitions. +From Mctt.Algorithmic.Subtyping Require Export Lemmas. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import Consequences.Rules. +From Mctt.Core.Semantic Require Import Consequences. +From Mctt.Frontend Require Import Elaborator. Import Domain_Notations. Lemma functional_alg_type_infer : forall {Γ A A' M}, @@ -31,7 +31,7 @@ Proof. Qed. #[local] -Hint Resolve functional_alg_type_infer : mcltt. +Hint Resolve functional_alg_type_infer : mctt. Ltac functional_alg_type_infer_rewrite_clear1 := let tactic_error o1 o2 := fail 3 "functional_alg_type_infer equality between" o1 "and" o2 "cannot be solved by mauto" in @@ -139,7 +139,7 @@ Proof with (f_equiv; mautosolve 4). Qed. #[export] -Hint Resolve alg_type_infer_normal : mcltt. +Hint Resolve alg_type_infer_normal : mctt. Lemma alg_type_check_typ_implies_alg_type_infer_typ : forall {Γ A i}, {{ ⊢ Γ }} -> @@ -158,7 +158,7 @@ Proof. Qed. #[export] -Hint Resolve alg_type_check_typ_implies_alg_type_infer_typ : mcltt. +Hint Resolve alg_type_check_typ_implies_alg_type_infer_typ : mctt. Lemma alg_type_check_pi_implies_alg_type_infer_pi : forall {Γ M A B i}, {{ ⊢ Γ }} -> @@ -197,7 +197,7 @@ Proof. Qed. #[export] -Hint Resolve alg_type_check_pi_implies_alg_type_infer_pi : mcltt. +Hint Resolve alg_type_check_pi_implies_alg_type_infer_pi : mctt. Lemma alg_type_check_subtyp : forall {Γ A A' M}, {{ Γ ⊢a M ⟸ A }} -> @@ -210,7 +210,7 @@ Proof. Qed. #[export] -Hint Resolve alg_type_check_subtyp : mcltt. +Hint Resolve alg_type_check_subtyp : mctt. Corollary alg_type_check_conv : forall {Γ i A A' M}, {{ Γ ⊢a M ⟸ A }} -> @@ -221,7 +221,7 @@ Proof. Qed. #[export] -Hint Resolve alg_type_check_conv : mcltt. +Hint Resolve alg_type_check_conv : mctt. Lemma alg_type_check_complete : forall {Γ A M}, user_exp M -> @@ -273,7 +273,7 @@ Proof. Qed. #[export] -Hint Resolve alg_type_check_complete : mcltt. +Hint Resolve alg_type_check_complete : mctt. Corollary alg_type_infer_complete : forall {Γ A M}, user_exp M -> @@ -287,7 +287,7 @@ Proof. Qed. #[export] -Hint Resolve alg_type_infer_complete : mcltt. +Hint Resolve alg_type_infer_complete : mctt. Corollary alg_type_infer_typ_complete : forall {Γ i A}, user_exp A -> @@ -298,7 +298,7 @@ Proof. Qed. #[export] -Hint Resolve alg_type_infer_typ_complete : mcltt. +Hint Resolve alg_type_infer_typ_complete : mctt. Corollary alg_type_infer_pi_complete : forall {Γ i A}, user_exp A -> @@ -309,4 +309,4 @@ Proof. Qed. #[export] -Hint Resolve alg_type_infer_pi_complete : mcltt. +Hint Resolve alg_type_infer_pi_complete : mctt. diff --git a/theories/Core/Base.v b/theories/Core/Base.v index ce40c12..762b019 100644 --- a/theories/Core/Base.v +++ b/theories/Core/Base.v @@ -1,6 +1,6 @@ -#[global] Declare Scope mcltt_scope. -#[global] Delimit Scope mcltt_scope with mcltt. -#[global] Bind Scope mcltt_scope with Sortclass. +#[global] Declare Scope mctt_scope. +#[global] Delimit Scope mctt_scope with mctt. +#[global] Bind Scope mctt_scope with Sortclass. #[global] Declare Custom Entry judg. diff --git a/theories/Core/Completeness.v b/theories/Core/Completeness.v index fa37afb..131d605 100644 --- a/theories/Core/Completeness.v +++ b/theories/Core/Completeness.v @@ -1,9 +1,9 @@ -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. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Export FundamentalTheorem. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Semantic Require Export NbE. +From Mctt.Core.Syntactic Require Export SystemOpt. Import Domain_Notations. Theorem completeness : forall {Γ M M' A}, diff --git a/theories/Core/Completeness/Consequences/Rules.v b/theories/Core/Completeness/Consequences/Rules.v index 15c1730..f6aa62d 100644 --- a/theories/Core/Completeness/Consequences/Rules.v +++ b/theories/Core/Completeness/Consequences/Rules.v @@ -1,8 +1,8 @@ From Coq Require Import RelationClasses. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core Require Export Completeness. -From Mcltt.Core.Semantic Require Import Realizability. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core Require Export Completeness. +From Mctt.Core.Semantic Require Import Realizability. Import Domain_Notations. Lemma ctxeq_nbe_eq : forall Γ Γ' M A, diff --git a/theories/Core/Completeness/Consequences/Types.v b/theories/Core/Completeness/Consequences/Types.v index f426b64..0af50b0 100644 --- a/theories/Core/Completeness/Consequences/Types.v +++ b/theories/Core/Completeness/Consequences/Types.v @@ -1,9 +1,9 @@ From Coq Require Import RelationClasses. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core Require Export Completeness. -From Mcltt.Core.Semantic Require Import Realizability. -From Mcltt.Core.Syntactic Require Export SystemOpt. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core Require Export Completeness. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Syntactic Require Export SystemOpt. Import Domain_Notations. Lemma exp_eq_typ_implies_eq_level : forall {Γ i j k}, @@ -25,7 +25,7 @@ Proof with mautosolve. reflexivity. Qed. #[export] -Hint Resolve exp_eq_typ_implies_eq_level : mcltt. +Hint Resolve exp_eq_typ_implies_eq_level : mctt. Inductive is_typ_constr : typ -> Prop := | typ_is_typ_constr : forall i, is_typ_constr {{{ Type@i }}} @@ -34,7 +34,7 @@ Inductive is_typ_constr : typ -> Prop := | var_is_typ_constr : forall x, is_typ_constr {{{ #x }}} . #[export] -Hint Constructors is_typ_constr : mcltt. +Hint Constructors is_typ_constr : mctt. Theorem is_typ_constr_and_exp_eq_var_implies_eq_var : forall Γ A x i, is_typ_constr A -> @@ -74,7 +74,7 @@ Proof. lia. Qed. #[export] -Hint Resolve is_typ_constr_and_exp_eq_var_implies_eq_var : mcltt. +Hint Resolve is_typ_constr_and_exp_eq_var_implies_eq_var : mctt. Theorem is_typ_constr_and_exp_eq_typ_implies_eq_typ : forall Γ A i j, is_typ_constr A -> @@ -100,7 +100,7 @@ Proof. reflexivity. Qed. #[export] -Hint Resolve is_typ_constr_and_exp_eq_typ_implies_eq_typ : mcltt. +Hint Resolve is_typ_constr_and_exp_eq_typ_implies_eq_typ : mctt. Theorem is_typ_constr_and_exp_eq_nat_implies_eq_nat : forall Γ A j, is_typ_constr A -> @@ -127,4 +127,4 @@ Proof. Qed. #[export] -Hint Resolve is_typ_constr_and_exp_eq_nat_implies_eq_nat : mcltt. +Hint Resolve is_typ_constr_and_exp_eq_nat_implies_eq_nat : mctt. diff --git a/theories/Core/Completeness/ContextCases.v b/theories/Core/Completeness/ContextCases.v index 531fb3e..65f9e33 100644 --- a/theories/Core/Completeness/ContextCases.v +++ b/theories/Core/Completeness/ContextCases.v @@ -1,8 +1,8 @@ From Coq Require Import Morphisms_Relations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import LogicalRelation UniverseCases. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import LogicalRelation UniverseCases. Import Domain_Notations. Proposition valid_ctx_empty : @@ -13,7 +13,7 @@ Proof. Qed. #[export] -Hint Resolve valid_ctx_empty : mcltt. +Hint Resolve valid_ctx_empty : mctt. Lemma rel_ctx_extend : forall {Γ Γ' A A' i}, {{ ⊨ Γ ≈ Γ' }} -> @@ -52,7 +52,7 @@ Proof. Qed. #[export] -Hint Resolve rel_ctx_extend rel_ctx_extend' : mcltt. +Hint Resolve rel_ctx_extend rel_ctx_extend' : mctt. Lemma rel_ctx_sub_empty : {{ SubE ⋅ <: ⋅ }}. @@ -76,4 +76,4 @@ Proof. Qed. #[export] -Hint Resolve rel_ctx_sub_empty rel_ctx_sub_extend : mcltt. +Hint Resolve rel_ctx_sub_empty rel_ctx_sub_extend : mctt. diff --git a/theories/Core/Completeness/EqualityCases.v b/theories/Core/Completeness/EqualityCases.v index 946bda5..559321a 100644 --- a/theories/Core/Completeness/EqualityCases.v +++ b/theories/Core/Completeness/EqualityCases.v @@ -1,9 +1,9 @@ From Coq Require Import Morphisms_Relations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import ContextCases LogicalRelation SubstitutionCases SubtypingCases TermStructureCases UniverseCases VariableCases. -From Mcltt.Core.Semantic Require Import Realizability. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import ContextCases LogicalRelation SubstitutionCases SubtypingCases TermStructureCases UniverseCases VariableCases. +From Mctt.Core.Semantic Require Import Realizability. Import Domain_Notations. Lemma rel_exp_eq_cong : forall {Γ i A A' M1 M1' M2 M2'}, @@ -30,7 +30,7 @@ Proof. per_univ_elem_econstructor; mauto 3; try solve_refl. Qed. #[export] -Hint Resolve rel_exp_eq_cong : mcltt. +Hint Resolve rel_exp_eq_cong : mctt. Lemma valid_exp_eq : forall {Γ i A M1 M2}, {{ Γ ⊨ A : Type@i }} -> @@ -40,7 +40,7 @@ Lemma valid_exp_eq : forall {Γ i A M1 M2}, Proof. mauto. Qed. #[export] -Hint Resolve valid_exp_eq : mcltt. +Hint Resolve valid_exp_eq : mctt. Lemma rel_exp_refl_cong : forall {Γ i A A' M M'}, {{ Γ ⊨ A ≈ A' : Type@i }} -> @@ -67,7 +67,7 @@ Proof. symmetry; mauto 3. Qed. #[export] -Hint Resolve rel_exp_refl_cong : mcltt. +Hint Resolve rel_exp_refl_cong : mctt. Lemma rel_exp_eq_sub : forall {Γ σ Δ i A M1 M2}, {{ Γ ⊨s σ : Δ }} -> @@ -97,7 +97,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_eq_sub : mcltt. +Hint Resolve rel_exp_eq_sub : mctt. Lemma rel_exp_refl_sub : forall {Γ σ Δ i A M}, {{ Γ ⊨s σ : Δ }} -> @@ -126,7 +126,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_refl_sub : mcltt. +Hint Resolve rel_exp_refl_sub : mctt. Lemma rel_exp_eqrec_sub : forall {Γ σ Δ i A M1 M2 j B BR N}, {{ Γ ⊨s σ : Δ }} -> @@ -208,7 +208,7 @@ Proof. It might be better to do some optimization first. *) Admitted. #[export] -Hint Resolve rel_exp_eqrec_sub : mcltt. +Hint Resolve rel_exp_eqrec_sub : mctt. Lemma rel_exp_eqrec_cong : forall {Γ i A A' M1 M1' M2 M2' j B B' BR BR' N N'}, {{ Γ ⊨ A : Type@i }} -> @@ -226,7 +226,7 @@ Lemma rel_exp_eqrec_cong : forall {Γ i A A' M1 M1' M2 M2' j B B' BR BR' N N'}, Proof. Admitted. #[export] -Hint Resolve rel_exp_eqrec_cong : mcltt. +Hint Resolve rel_exp_eqrec_cong : mctt. Lemma rel_exp_eqrec_beta : forall {Γ i A M j B BR}, {{ Γ ⊨ A : Type@i }} -> @@ -239,4 +239,4 @@ Lemma rel_exp_eqrec_beta : forall {Γ i A M j B BR}, Proof. Admitted. #[export] -Hint Resolve rel_exp_eqrec_beta : mcltt. +Hint Resolve rel_exp_eqrec_beta : mctt. diff --git a/theories/Core/Completeness/FunctionCases.v b/theories/Core/Completeness/FunctionCases.v index ebe1e01..1c34693 100644 --- a/theories/Core/Completeness/FunctionCases.v +++ b/theories/Core/Completeness/FunctionCases.v @@ -1,8 +1,8 @@ From Coq Require Import Morphisms_Relations Relation_Definitions. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import LogicalRelation TermStructureCases UniverseCases. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import LogicalRelation TermStructureCases UniverseCases. Import Domain_Notations. Lemma rel_exp_of_pi_inversion : forall {Γ M M' A B}, @@ -115,7 +115,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_pi_cong : mcltt. +Hint Resolve rel_exp_pi_cong : mctt. Lemma rel_exp_pi_sub : forall {i Γ σ Δ A B}, {{ Γ ⊨s σ : Δ }} -> @@ -149,7 +149,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_pi_sub : mcltt. +Hint Resolve rel_exp_pi_sub : mctt. Lemma rel_exp_fn_cong : forall {i Γ A A' B M M'}, {{ Γ ⊨ A ≈ A' : Type@i }} -> @@ -185,7 +185,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_fn_cong : mcltt. +Hint Resolve rel_exp_fn_cong : mctt. Lemma rel_exp_fn_sub : forall {Γ σ Δ A M B}, {{ Γ ⊨s σ : Δ }} -> @@ -222,7 +222,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_fn_sub : mcltt. +Hint Resolve rel_exp_fn_sub : mctt. Lemma rel_exp_app_cong : forall {Γ M M' A B N N'}, {{ Γ ⊨ M ≈ M' : Π A B }} -> @@ -250,7 +250,7 @@ Proof with intuition. Qed. #[export] -Hint Resolve rel_exp_app_cong : mcltt. +Hint Resolve rel_exp_app_cong : mctt. Lemma rel_exp_app_sub : forall {Γ σ Δ M A B N}, {{ Γ ⊨s σ : Δ }} -> @@ -277,7 +277,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_app_sub : mcltt. +Hint Resolve rel_exp_app_sub : mctt. Lemma rel_exp_pi_beta : forall {Γ A M B N}, {{ Γ , A ⊨ M : B }} -> @@ -303,7 +303,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_pi_beta : mcltt. +Hint Resolve rel_exp_pi_beta : mctt. Lemma rel_exp_pi_eta : forall {Γ M A B}, {{ Γ ⊨ M : Π A B }} -> @@ -325,4 +325,4 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_pi_eta : mcltt. +Hint Resolve rel_exp_pi_eta : mctt. diff --git a/theories/Core/Completeness/FundamentalTheorem.v b/theories/Core/Completeness/FundamentalTheorem.v index c5c06ce..6c61e97 100644 --- a/theories/Core/Completeness/FundamentalTheorem.v +++ b/theories/Core/Completeness/FundamentalTheorem.v @@ -1,5 +1,5 @@ -From Mcltt Require Import Base LibTactics. -From Mcltt.Core.Completeness Require Import +From Mctt Require Import Base LibTactics. +From Mctt.Core.Completeness Require Import ContextCases EqualityCases FunctionCases @@ -9,8 +9,8 @@ From Mcltt.Core.Completeness Require Import UniverseCases VariableCases SubtypingCases. -From Mcltt.Core.Completeness Require Export LogicalRelation. -From Mcltt.Core.Syntactic Require Export SystemOpt. +From Mctt.Core.Completeness Require Export LogicalRelation. +From Mctt.Core.Syntactic Require Export SystemOpt. Import Domain_Notations. Section completeness_fundamental. diff --git a/theories/Core/Completeness/LogicalRelation.v b/theories/Core/Completeness/LogicalRelation.v index 3e03947..ab7ea24 100644 --- a/theories/Core/Completeness/LogicalRelation.v +++ b/theories/Core/Completeness/LogicalRelation.v @@ -1 +1 @@ -From Mcltt.Core.Completeness.LogicalRelation Require Export Definitions Lemmas Tactics. +From Mctt.Core.Completeness.LogicalRelation Require Export Definitions Lemmas Tactics. diff --git a/theories/Core/Completeness/LogicalRelation/Definitions.v b/theories/Core/Completeness/LogicalRelation/Definitions.v index b362478..63e2d2c 100644 --- a/theories/Core/Completeness/LogicalRelation/Definitions.v +++ b/theories/Core/Completeness/LogicalRelation/Definitions.v @@ -1,6 +1,6 @@ From Coq Require Import Relations. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Export PER. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Export PER. Import Domain_Notations. Inductive rel_exp M ρ M' ρ' (R : relation domain) : Prop := @@ -8,7 +8,7 @@ Inductive rel_exp M ρ M' ρ' (R : relation domain) : Prop := #[global] Arguments mk_rel_exp {_ _ _ _ _}. #[export] -Hint Constructors rel_exp : mcltt. +Hint Constructors rel_exp : mctt. Definition rel_exp_under_ctx Γ A M M' := exists env_rel, @@ -22,16 +22,16 @@ Definition valid_exp_under_ctx Γ A M := rel_exp_under_ctx Γ A M M. #[global] Arguments valid_exp_under_ctx _ _ _ /. #[export] -Hint Transparent valid_exp_under_ctx : mcltt. +Hint Transparent valid_exp_under_ctx : mctt. #[export] -Hint Unfold valid_exp_under_ctx : mcltt. +Hint Unfold valid_exp_under_ctx : mctt. Inductive rel_sub σ ρ σ' ρ' (R : relation env) : Prop := | mk_rel_sub : forall ρσ ρ'σ', {{ ⟦ σ ⟧s ρ ↘ ρσ }} -> {{ ⟦ σ' ⟧s ρ' ↘ ρ'σ' }} -> {{ Dom ρσ ≈ ρ'σ' ∈ R }} -> rel_sub σ ρ σ' ρ' R. #[global] Arguments mk_rel_sub {_ _ _ _ _ _}. #[export] -Hint Constructors rel_sub : mcltt. +Hint Constructors rel_sub : mctt. Definition rel_sub_under_ctx Γ Δ σ σ' := exists env_rel, @@ -45,9 +45,9 @@ Definition valid_sub_under_ctx Γ Δ σ := rel_sub_under_ctx Γ Δ σ σ. #[global] Arguments valid_sub_under_ctx _ _ _ /. #[export] -Hint Transparent valid_sub_under_ctx : mcltt. +Hint Transparent valid_sub_under_ctx : mctt. #[export] -Hint Unfold valid_sub_under_ctx : mcltt. +Hint Unfold valid_sub_under_ctx : mctt. Definition subtyp_under_ctx Γ M M' := exists env_rel, diff --git a/theories/Core/Completeness/LogicalRelation/Lemmas.v b/theories/Core/Completeness/LogicalRelation/Lemmas.v index 6a1019d..042e0c0 100644 --- a/theories/Core/Completeness/LogicalRelation/Lemmas.v +++ b/theories/Core/Completeness/LogicalRelation/Lemmas.v @@ -1,8 +1,8 @@ From Coq Require Import Morphisms Morphisms_Relations RelationClasses Relation_Definitions. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness.LogicalRelation Require Import Definitions Tactics. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness.LogicalRelation Require Import Definitions Tactics. Import Domain_Notations. Add Parametric Morphism M ρ M' ρ' : (rel_exp M ρ M' ρ') @@ -30,7 +30,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_implies_rel_typ : mcltt. +Hint Resolve rel_exp_implies_rel_typ : mctt. Lemma rel_typ_implies_rel_exp : forall {i A ρ A' ρ' R}, rel_typ i A ρ A' ρ' R -> @@ -42,7 +42,7 @@ Proof. Qed. #[export] -Hint Resolve rel_typ_implies_rel_exp : mcltt. +Hint Resolve rel_typ_implies_rel_exp : mctt. Lemma rel_exp_clean_inversion : forall {Γ env_rel A M M'}, {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }} -> diff --git a/theories/Core/Completeness/LogicalRelation/Tactics.v b/theories/Core/Completeness/LogicalRelation/Tactics.v index d9d073e..7490d2f 100644 --- a/theories/Core/Completeness/LogicalRelation/Tactics.v +++ b/theories/Core/Completeness/LogicalRelation/Tactics.v @@ -1,6 +1,6 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Import PER. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Import PER. Import Domain_Notations. Ltac eexists_rel_exp := diff --git a/theories/Core/Completeness/NatCases.v b/theories/Core/Completeness/NatCases.v index 34c20d3..99eedcb 100644 --- a/theories/Core/Completeness/NatCases.v +++ b/theories/Core/Completeness/NatCases.v @@ -1,9 +1,9 @@ From Coq Require Import Morphisms_Relations. -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. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import LogicalRelation SubstitutionCases TermStructureCases UniverseCases. +From Mctt.Core.Semantic Require Import Realizability. Import Domain_Notations. Lemma rel_exp_of_nat_inversion : forall {Γ M M'}, @@ -40,7 +40,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_of_nat : mcltt. +Hint Resolve rel_exp_of_nat : mctt. Ltac eexists_rel_exp_of_nat := apply rel_exp_of_nat; @@ -61,7 +61,7 @@ Proof. Qed. #[export] -Hint Resolve valid_exp_nat : mcltt. +Hint Resolve valid_exp_nat : mctt. Lemma rel_exp_nat_sub : forall {Γ σ i Δ}, {{ Γ ⊨s σ : Δ }} -> @@ -79,7 +79,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_nat_sub : mcltt. +Hint Resolve rel_exp_nat_sub : mctt. Lemma valid_exp_zero : forall {Γ}, {{ ⊨ Γ }} -> @@ -92,7 +92,7 @@ Proof. Qed. #[export] -Hint Resolve valid_exp_zero : mcltt. +Hint Resolve valid_exp_zero : mctt. Lemma rel_exp_zero_sub : forall {Γ σ Δ}, {{ Γ ⊨s σ : Δ }} -> @@ -107,7 +107,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_zero_sub : mcltt. +Hint Resolve rel_exp_zero_sub : mctt. Lemma rel_exp_succ_sub : forall {Γ σ Δ M}, {{ Γ ⊨s σ : Δ }} -> @@ -126,7 +126,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_succ_sub : mcltt. +Hint Resolve rel_exp_succ_sub : mctt. Lemma rel_exp_succ_cong : forall {Γ M M'}, {{ Γ ⊨ M ≈ M' : ℕ }} -> @@ -141,7 +141,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_succ_cong : mcltt. +Hint Resolve rel_exp_succ_cong : mctt. Lemma rel_exp_of_sub_id_zero_inversion : forall {Γ M M' A}, {{ Γ ⊨ M ≈ M' : A[Id,,zero] }} -> @@ -498,7 +498,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_natrec_cong : mcltt. +Hint Resolve rel_exp_natrec_cong : mctt. Lemma eval_natrec_sub_rel : forall {Γ env_relΓ σ Δ env_relΔ MZ MZ' MS MS' A A' i m m'}, {{ DF Γ ≈ Γ ∈ per_ctx_env ↘ env_relΓ }} -> @@ -676,7 +676,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_natrec_sub : mcltt. +Hint Resolve rel_exp_natrec_sub : mctt. Lemma rel_exp_nat_beta_zero : forall {Γ MZ MS A}, {{ Γ ⊨ MZ : A[Id,,zero] }} -> @@ -711,7 +711,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_nat_beta_zero : mcltt. +Hint Resolve rel_exp_nat_beta_zero : mctt. Lemma rel_exp_nat_beta_succ_rel_typ : forall {Γ env_relΓ A i M}, {{ DF Γ ≈ Γ ∈ per_ctx_env ↘ env_relΓ }} -> @@ -768,4 +768,4 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_nat_beta_succ : mcltt. +Hint Resolve rel_exp_nat_beta_succ : mctt. diff --git a/theories/Core/Completeness/SubstitutionCases.v b/theories/Core/Completeness/SubstitutionCases.v index 8021b6f..fcb14c1 100644 --- a/theories/Core/Completeness/SubstitutionCases.v +++ b/theories/Core/Completeness/SubstitutionCases.v @@ -1,8 +1,8 @@ From Coq Require Import Morphisms_Relations RelationClasses. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import ContextCases LogicalRelation UniverseCases. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import ContextCases LogicalRelation UniverseCases. Import Domain_Notations. Lemma rel_sub_id : forall {Γ}, @@ -14,7 +14,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_id : mcltt. +Hint Resolve rel_sub_id : mctt. Lemma rel_sub_weaken : forall {Γ A}, {{ ⊨ Γ, A }} -> @@ -29,7 +29,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_weaken : mcltt. +Hint Resolve rel_sub_weaken : mctt. Lemma rel_sub_compose_cong : forall {Γ τ τ' Γ' σ σ' Γ''}, {{ Γ ⊨s τ ≈ τ' : Γ' }} -> @@ -47,7 +47,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_compose_cong : mcltt. +Hint Resolve rel_sub_compose_cong : mctt. Lemma rel_sub_extend_cong : forall {i Γ M M' σ σ' Δ A}, {{ Γ ⊨s σ ≈ σ' : Δ }} -> @@ -73,7 +73,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_extend_cong : mcltt. +Hint Resolve rel_sub_extend_cong : mctt. Lemma rel_sub_id_compose_right : forall {Γ σ Δ}, {{ Γ ⊨s σ : Δ }} -> @@ -87,7 +87,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_id_compose_right : mcltt. +Hint Resolve rel_sub_id_compose_right : mctt. Lemma rel_sub_id_compose_left : forall {Γ σ Δ}, {{ Γ ⊨s σ : Δ }} -> @@ -101,7 +101,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_id_compose_left : mcltt. +Hint Resolve rel_sub_id_compose_left : mctt. Lemma rel_sub_compose_assoc : forall {Γ σ Γ' σ' Γ'' σ'' Γ'''}, {{ Γ' ⊨s σ : Γ }} -> @@ -123,7 +123,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_compose_assoc : mcltt. +Hint Resolve rel_sub_compose_assoc : mctt. Lemma rel_sub_extend_compose : forall {Γ τ Γ' M σ Γ'' A i}, {{ Γ' ⊨s σ : Γ'' }} -> @@ -153,7 +153,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_extend_compose : mcltt. +Hint Resolve rel_sub_extend_compose : mctt. Lemma rel_sub_p_extend : forall {Γ' M σ Γ A}, {{ Γ' ⊨s σ : Γ }} -> @@ -174,7 +174,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_p_extend : mcltt. +Hint Resolve rel_sub_p_extend : mctt. Lemma rel_sub_extend : forall {Γ' σ Γ A}, {{ Γ' ⊨s σ : Γ, A }} -> @@ -195,7 +195,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_extend : mcltt. +Hint Resolve rel_sub_extend : mctt. Lemma rel_sub_sym : forall {Γ σ σ' Δ}, {{ Γ ⊨s σ ≈ σ' : Δ }} -> @@ -211,7 +211,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_sym : mcltt. +Hint Resolve rel_sub_sym : mctt. Lemma rel_sub_trans : forall {Γ σ σ' σ'' Δ}, {{ Γ ⊨s σ ≈ σ' : Δ }} -> @@ -231,7 +231,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_trans : mcltt. +Hint Resolve rel_sub_trans : mctt. #[export] Instance rel_sub_PER {Γ A} : PER (rel_sub_under_ctx Γ A). @@ -253,7 +253,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_sub_conv : mcltt. +Hint Resolve rel_sub_conv : mctt. Lemma presup_rel_sub : forall {Γ σ σ' Δ}, {{ Γ ⊨s σ ≈ σ' : Δ }} -> @@ -284,4 +284,4 @@ Proof. Qed. #[export] -Hint Resolve rel_sub_eq_subtyp : mcltt. +Hint Resolve rel_sub_eq_subtyp : mctt. diff --git a/theories/Core/Completeness/SubtypingCases.v b/theories/Core/Completeness/SubtypingCases.v index ddbef96..63e6ed9 100644 --- a/theories/Core/Completeness/SubtypingCases.v +++ b/theories/Core/Completeness/SubtypingCases.v @@ -1,8 +1,8 @@ From Coq Require Import Morphisms_Relations RelationClasses. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import LogicalRelation FunctionCases. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import LogicalRelation FunctionCases. Import Domain_Notations. Lemma subtyp_refl : forall Γ M M' i, @@ -147,4 +147,4 @@ Proof. Qed. #[export] -Hint Resolve subtyp_refl subtyp_trans subtyp_univ subtyp_pi : mcltt. +Hint Resolve subtyp_refl subtyp_trans subtyp_univ subtyp_pi : mctt. diff --git a/theories/Core/Completeness/TermStructureCases.v b/theories/Core/Completeness/TermStructureCases.v index 5ccccd0..e348969 100644 --- a/theories/Core/Completeness/TermStructureCases.v +++ b/theories/Core/Completeness/TermStructureCases.v @@ -1,8 +1,8 @@ From Coq Require Import Morphisms_Relations RelationClasses. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import LogicalRelation UniverseCases. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import LogicalRelation UniverseCases. Import Domain_Notations. Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ}, @@ -36,7 +36,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_sub_cong : mcltt. +Hint Resolve rel_exp_sub_cong : mctt. Lemma rel_exp_sub_id : forall {Γ M A}, {{ Γ ⊨ M : A }} -> @@ -54,7 +54,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_sub_id : mcltt. +Hint Resolve rel_exp_sub_id : mctt. Lemma rel_exp_sub_compose : forall {Γ τ Γ' σ Γ'' M A}, {{ Γ ⊨s τ : Γ' }} -> @@ -84,7 +84,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_sub_compose : mcltt. +Hint Resolve rel_exp_sub_compose : mctt. Lemma rel_exp_conv : forall {Γ M M' A A' i}, {{ Γ ⊨ M ≈ M' : A }} -> @@ -108,7 +108,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_conv : mcltt. +Hint Resolve rel_exp_conv : mctt. Lemma rel_exp_sym : forall {Γ M M' A}, {{ Γ ⊨ M ≈ M' : A }} -> @@ -129,7 +129,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_sym : mcltt. +Hint Resolve rel_exp_sym : mctt. Lemma rel_exp_trans : forall {Γ M1 M2 M3 A}, {{ Γ ⊨ M1 ≈ M2 : A }} -> @@ -153,7 +153,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_trans : mcltt. +Hint Resolve rel_exp_trans : mctt. #[export] Instance rel_exp_PER {Γ A} : PER (rel_exp_under_ctx Γ A). @@ -207,4 +207,4 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_eq_subtyp : mcltt. +Hint Resolve rel_exp_eq_subtyp : mctt. diff --git a/theories/Core/Completeness/UniverseCases.v b/theories/Core/Completeness/UniverseCases.v index 943cac4..69a7f7e 100644 --- a/theories/Core/Completeness/UniverseCases.v +++ b/theories/Core/Completeness/UniverseCases.v @@ -1,8 +1,8 @@ From Coq Require Import Morphisms_Relations RelationClasses. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import LogicalRelation. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import LogicalRelation. Import Domain_Notations. Lemma rel_exp_of_typ_inversion1 : forall {Γ A A' i}, @@ -82,7 +82,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_of_typ : mcltt. +Hint Resolve rel_exp_of_typ : mctt. Ltac eexists_rel_exp_of_typ := unshelve eapply (rel_exp_of_typ _); @@ -103,7 +103,7 @@ Proof. Qed. #[export] -Hint Resolve valid_exp_typ : mcltt. +Hint Resolve valid_exp_typ : mctt. Lemma rel_exp_typ_sub : forall {i Γ σ Δ}, {{ Γ ⊨s σ : Δ }} -> @@ -121,7 +121,7 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_typ_sub : mcltt. +Hint Resolve rel_exp_typ_sub : mctt. Lemma rel_exp_cumu : forall {i Γ A A'}, {{ Γ ⊨ A ≈ A' : Type@i }} -> @@ -138,4 +138,4 @@ Proof. Qed. #[export] -Hint Resolve rel_exp_cumu : mcltt. +Hint Resolve rel_exp_cumu : mctt. diff --git a/theories/Core/Completeness/VariableCases.v b/theories/Core/Completeness/VariableCases.v index ff62637..74b3dd6 100644 --- a/theories/Core/Completeness/VariableCases.v +++ b/theories/Core/Completeness/VariableCases.v @@ -1,9 +1,9 @@ From Coq Require Import Morphisms_Relations. -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. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import LogicalRelation. +From Mctt.Core.Syntactic Require Import SystemOpt. Import Domain_Notations. Lemma valid_lookup : forall {Γ x A env_rel} @@ -42,7 +42,7 @@ Proof. Qed. #[export] -Hint Resolve valid_exp_var : mcltt. +Hint Resolve valid_exp_var : mctt. Lemma rel_exp_var_0_sub : forall {Γ M σ Δ A}, {{ Γ ⊨s σ : Δ }} -> @@ -64,7 +64,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_var_0_sub : mcltt. +Hint Resolve rel_exp_var_0_sub : mctt. Lemma rel_exp_var_S_sub : forall {Γ M σ Δ A x B}, {{ Γ ⊨s σ : Δ }} -> @@ -90,7 +90,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_var_S_sub : mcltt. +Hint Resolve rel_exp_var_S_sub : mctt. Lemma rel_exp_var_weaken : forall {Γ B x A}, {{ ⊨ Γ, B }} -> @@ -115,4 +115,4 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve rel_exp_var_weaken : mcltt. +Hint Resolve rel_exp_var_weaken : mctt. diff --git a/theories/Core/Semantic/Consequences.v b/theories/Core/Semantic/Consequences.v index 4cef9f7..9854014 100644 --- a/theories/Core/Semantic/Consequences.v +++ b/theories/Core/Semantic/Consequences.v @@ -1,7 +1,7 @@ -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. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core Require Export Soundness. +From Mctt.Core.Completeness.Consequences Require Export Types. Import Domain_Notations. Lemma idempotent_nbe_ty : forall {Γ i A B C}, @@ -16,7 +16,7 @@ Proof. reflexivity. Qed. #[export] -Hint Resolve idempotent_nbe_ty : mcltt. +Hint Resolve idempotent_nbe_ty : mctt. Lemma adjust_exp_eq_level : forall {Γ A A' i j}, {{ Γ ⊢ A ≈ A' : Type@i }} -> @@ -72,21 +72,21 @@ Proof. do 2 eexists; mauto 4. Qed. #[export] -Hint Resolve nf_of_pi : mcltt. +Hint Resolve nf_of_pi : mctt. Theorem canonical_form_of_pi : forall {M A B}, {{ ⋅ ⊢ M : Π A B }} -> exists W1 W2, nbe {{{ ⋅ }}} M {{{ Π A B }}} n{{{ λ W1 W2 }}}. Proof. mauto 3. Qed. #[export] -Hint Resolve canonical_form_of_pi : mcltt. +Hint Resolve canonical_form_of_pi : mctt. Inductive canonical_nat : nf -> Prop := | canonical_nat_zero : canonical_nat n{{{ zero }}} | canonical_nat_succ : forall W, canonical_nat W -> canonical_nat n{{{ succ W }}} . #[export] -Hint Constructors canonical_nat : mcltt. +Hint Constructors canonical_nat : mctt. Theorem canonical_form_of_nat : forall {M}, {{ ⋅ ⊢ M : ℕ }} -> @@ -105,7 +105,7 @@ Proof with mautosolve 4. - match_by_head1 (wf_exp {{{ ⋅ }}} {{{ ℕ }}}) ltac:(fun H => contradict H)... Qed. #[export] -Hint Resolve canonical_form_of_nat : mcltt. +Hint Resolve canonical_form_of_nat : mctt. Theorem canonical_form_of_typ : forall {i M}, {{ ⋅ ⊢ M : Type@i }} -> @@ -124,7 +124,7 @@ Proof with mautosolve 4. match_by_head1 (wf_exp {{{ ⋅ }}} {{{ Type@i }}}) ltac:(fun H => contradict H)... Qed. #[export] -Hint Resolve canonical_form_of_typ : mcltt. +Hint Resolve canonical_form_of_typ : mctt. Lemma subtyp_spec : forall {Γ A B}, {{ Γ ⊢ A ⊆ B }} -> @@ -164,7 +164,7 @@ Proof with (congruence + firstorder (mautosolve 4 + lia)). Qed. #[export] -Hint Resolve subtyp_spec : mcltt. +Hint Resolve subtyp_spec : mctt. Lemma consistency_ne_helper : forall {i A A'} {W : ne}, is_typ_constr A' -> diff --git a/theories/Core/Semantic/Domain.v b/theories/Core/Semantic/Domain.v index 401595a..73047b6 100644 --- a/theories/Core/Semantic/Domain.v +++ b/theories/Core/Semantic/Domain.v @@ -1,6 +1,6 @@ From Equations Require Import Equations. -From Mcltt.Core.Syntactic Require Export Syntax. +From Mctt.Core.Syntactic Require Export Syntax. Reserved Notation "'env'". @@ -46,33 +46,33 @@ Arguments drop_env _ _ /. Transparent drop_env. #[global] Declare Custom Entry domain. -#[global] Bind Scope mcltt_scope with domain. +#[global] Bind Scope mctt_scope with domain. Module Domain_Notations. Export Syntax_Notations. - Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{' x '}}}'") : mcltt_scope. - Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : mcltt_scope. - Notation "'^' x" := x (in custom domain at level 0, x constr at level 0) : mcltt_scope. - Notation "x" := x (in custom domain at level 0, x ident) : mcltt_scope. - Notation "'𝕌' @ n" := (d_univ n) (in custom domain at level 0, n constr at level 0) : mcltt_scope. - Notation "'ℕ'" := d_nat (in custom domain) : mcltt_scope. - Notation "'zero'" := d_zero (in custom domain at level 0) : mcltt_scope. - Notation "'succ' m" := (d_succ m) (in custom domain at level 30, m custom domain at level 30) : mcltt_scope. - Notation "'rec' m 'under' ρ 'return' P | 'zero' -> mz | 'succ' -> MS 'end'" := (d_natrec ρ P mz MS m) (in custom domain at level 0, P custom exp at level 60, mz custom domain at level 60, MS custom exp at level 60, ρ custom domain at level 60, m custom domain at level 60) : mcltt_scope. - Notation "'Π' a ρ B" := (d_pi a ρ B) (in custom domain at level 0, a custom domain at level 30, ρ custom domain at level 0, B custom exp at level 30) : mcltt_scope. - Notation "'λ' ρ M" := (d_fn ρ M) (in custom domain at level 0, ρ custom domain at level 30, M custom exp at level 30) : mcltt_scope. - Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : mcltt_scope. - Notation "'Eq' a m n" := (d_eq a m n) (in custom domain at level 1, a custom domain at level 30, m custom domain at level 35, n custom domain at level 40) : mcltt_scope. - Notation "'refl' m" := (d_refl m) (in custom domain at level 1, m custom domain at level 40) : mcltt_scope. - Notation "'eqrec' n 'under' ρ 'as' 'Eq' a m1 m2 'return' B | 'refl' -> BR 'end'" := (d_eqrec ρ a B BR m1 m2 n) (in custom domain at level 0, a custom domain at level 30, B custom domain at level 60, BR custom domain at level 60, m1 custom domain at level 35, m2 custom domain at level 40, n custom domain at level 60) : mcltt_scope. - Notation "'!' n" := (d_var n) (in custom domain at level 0, n constr at level 0) : mcltt_scope. - Notation "'⇑' a m" := (d_neut a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : mcltt_scope. - Notation "'⇓' a m" := (d_dom a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : mcltt_scope. - Notation "'⇑!' a n" := (d_neut a (d_var n)) (in custom domain at level 0, a custom domain at level 30, n constr at level 0) : mcltt_scope. + Notation "'d{{{' x '}}}'" := x (at level 0, x custom domain at level 99, format "'d{{{' x '}}}'") : mctt_scope. + Notation "( x )" := x (in custom domain at level 0, x custom domain at level 60) : mctt_scope. + Notation "'^' x" := x (in custom domain at level 0, x constr at level 0) : mctt_scope. + Notation "x" := x (in custom domain at level 0, x ident) : mctt_scope. + Notation "'𝕌' @ n" := (d_univ n) (in custom domain at level 0, n constr at level 0) : mctt_scope. + Notation "'ℕ'" := d_nat (in custom domain) : mctt_scope. + Notation "'zero'" := d_zero (in custom domain at level 0) : mctt_scope. + Notation "'succ' m" := (d_succ m) (in custom domain at level 30, m custom domain at level 30) : mctt_scope. + Notation "'rec' m 'under' ρ 'return' P | 'zero' -> mz | 'succ' -> MS 'end'" := (d_natrec ρ P mz MS m) (in custom domain at level 0, P custom exp at level 60, mz custom domain at level 60, MS custom exp at level 60, ρ custom domain at level 60, m custom domain at level 60) : mctt_scope. + Notation "'Π' a ρ B" := (d_pi a ρ B) (in custom domain at level 0, a custom domain at level 30, ρ custom domain at level 0, B custom exp at level 30) : mctt_scope. + Notation "'λ' ρ M" := (d_fn ρ M) (in custom domain at level 0, ρ custom domain at level 30, M custom exp at level 30) : mctt_scope. + Notation "f x .. y" := (d_app .. (d_app f x) .. y) (in custom domain at level 40, f custom domain, x custom domain at next level, y custom domain at next level) : mctt_scope. + Notation "'Eq' a m n" := (d_eq a m n) (in custom domain at level 1, a custom domain at level 30, m custom domain at level 35, n custom domain at level 40) : mctt_scope. + Notation "'refl' m" := (d_refl m) (in custom domain at level 1, m custom domain at level 40) : mctt_scope. + Notation "'eqrec' n 'under' ρ 'as' 'Eq' a m1 m2 'return' B | 'refl' -> BR 'end'" := (d_eqrec ρ a B BR m1 m2 n) (in custom domain at level 0, a custom domain at level 30, B custom domain at level 60, BR custom domain at level 60, m1 custom domain at level 35, m2 custom domain at level 40, n custom domain at level 60) : mctt_scope. + Notation "'!' n" := (d_var n) (in custom domain at level 0, n constr at level 0) : mctt_scope. + Notation "'⇑' a m" := (d_neut a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : mctt_scope. + Notation "'⇓' a m" := (d_dom a m) (in custom domain at level 0, a custom domain at level 30, m custom domain at level 30) : mctt_scope. + Notation "'⇑!' a n" := (d_neut a (d_var n)) (in custom domain at level 0, a custom domain at level 30, n constr at level 0) : mctt_scope. - Notation "ρ ↦ m" := (extend_env ρ m) (in custom domain at level 20, left associativity) : mcltt_scope. - Notation "ρ '↯'" := (drop_env ρ) (in custom domain at level 10, ρ custom domain) : mcltt_scope. + Notation "ρ ↦ m" := (extend_env ρ m) (in custom domain at level 20, left associativity) : mctt_scope. + Notation "ρ '↯'" := (drop_env ρ) (in custom domain at level 10, ρ custom domain) : mctt_scope. End Domain_Notations. Import Domain_Notations. diff --git a/theories/Core/Semantic/Evaluation.v b/theories/Core/Semantic/Evaluation.v index e7e5807..5d18d19 100644 --- a/theories/Core/Semantic/Evaluation.v +++ b/theories/Core/Semantic/Evaluation.v @@ -1 +1 @@ -From Mcltt.Core.Semantic.Evaluation Require Export Definitions Lemmas Tactics. +From Mctt.Core.Semantic.Evaluation Require Export Definitions Lemmas Tactics. diff --git a/theories/Core/Semantic/Evaluation/Definitions.v b/theories/Core/Semantic/Evaluation/Definitions.v index 17d6b03..47ffb5c 100644 --- a/theories/Core/Semantic/Evaluation/Definitions.v +++ b/theories/Core/Semantic/Evaluation/Definitions.v @@ -1,5 +1,5 @@ -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Export Domain. +From Mctt.Core Require Import Base. +From Mctt.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). @@ -114,4 +114,4 @@ Combined Scheme eval_mut_ind from eval_sub_mut_ind. #[export] -Hint Constructors eval_exp eval_natrec eval_app eval_eqrec eval_sub : mcltt. +Hint Constructors eval_exp eval_natrec eval_app eval_eqrec eval_sub : mctt. diff --git a/theories/Core/Semantic/Evaluation/Lemmas.v b/theories/Core/Semantic/Evaluation/Lemmas.v index e388d4b..78732d1 100644 --- a/theories/Core/Semantic/Evaluation/Lemmas.v +++ b/theories/Core/Semantic/Evaluation/Lemmas.v @@ -1,8 +1,8 @@ From Coq Require Import Lia PeanoNat Relations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic.Evaluation Require Import Definitions. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic.Evaluation Require Import Definitions. Import Domain_Notations. Section functional_eval. @@ -79,7 +79,7 @@ Section functional_eval. End functional_eval. #[export] -Hint Resolve functional_eval_exp functional_eval_natrec functional_eval_app functional_eval_eqrec functional_eval_sub : mcltt. +Hint Resolve functional_eval_exp functional_eval_natrec functional_eval_app functional_eval_eqrec functional_eval_sub : mctt. Ltac functional_eval_rewrite_clear1 := let tactic_error o1 o2 := fail 3 "functional_eval equality between" o1 "and" o2 "cannot be solved by mauto" in diff --git a/theories/Core/Semantic/Evaluation/Tactics.v b/theories/Core/Semantic/Evaluation/Tactics.v index 1c1508e..a5c84ff 100644 --- a/theories/Core/Semantic/Evaluation/Tactics.v +++ b/theories/Core/Semantic/Evaluation/Tactics.v @@ -1,6 +1,6 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic.Evaluation Require Import Definitions Lemmas. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic.Evaluation Require Import Definitions Lemmas. Import Domain_Notations. Ltac simplify_evals := diff --git a/theories/Core/Semantic/NbE.v b/theories/Core/Semantic/NbE.v index a13076f..0a754d1 100644 --- a/theories/Core/Semantic/NbE.v +++ b/theories/Core/Semantic/NbE.v @@ -1,7 +1,7 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Export Domain Evaluation Readback. -From Mcltt.Core.Syntactic Require Export System. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Export Domain Evaluation Readback. +From Mctt.Core.Syntactic Require Export System. Import Domain_Notations. Generalizable All Variables. @@ -14,7 +14,7 @@ Inductive initial_env : ctx -> env -> Prop := initial_env (A :: Γ) d{{{ ρ ↦ ⇑! a (length Γ) }}}). #[export] -Hint Constructors initial_env : mcltt. +Hint Constructors initial_env : mctt. Lemma functional_initial_env : forall Γ ρ, initial_env Γ ρ -> @@ -29,7 +29,7 @@ Proof. Qed. #[export] -Hint Resolve functional_initial_env : mcltt. +Hint Resolve functional_initial_env : mctt. (** In the following spec, we do not care (for now) whether [a] is the evaluation result of A or not. @@ -46,7 +46,7 @@ Proof. Qed. #[export] -Hint Resolve initial_env_spec : mcltt. +Hint Resolve initial_env_spec : mctt. Ltac functional_initial_env_rewrite_clear1 := let tactic_error o1 o2 := fail 3 "functional_initial_env equality between" o1 "and" o2 "cannot be solved by mauto" in @@ -65,7 +65,7 @@ Inductive nbe : ctx -> exp -> typ -> nf -> Prop := nbe Γ M A w ). #[export] -Hint Constructors nbe : mcltt. +Hint Constructors nbe : mctt. Lemma functional_nbe : forall Γ M A w w', nbe Γ M A w -> @@ -81,7 +81,7 @@ Proof. Qed. #[export] -Hint Resolve functional_nbe : mcltt. +Hint Resolve functional_nbe : mctt. Lemma nbe_cumu : forall {Γ A i W}, nbe Γ A {{{ Type@i }}} W -> @@ -120,7 +120,7 @@ Proof. Qed. #[export] -Hint Resolve lift_nbe_max_left lift_nbe_max_right : mcltt. +Hint Resolve lift_nbe_max_left lift_nbe_max_right : mctt. Lemma functional_nbe_of_typ : forall Γ A i j W W', nbe Γ A {{{ Type@i }}} W -> @@ -131,7 +131,7 @@ Proof. Qed. #[export] -Hint Resolve functional_nbe_of_typ : mcltt. +Hint Resolve functional_nbe_of_typ : mctt. Inductive nbe_ty : ctx -> typ -> nf -> Prop := @@ -142,7 +142,7 @@ Inductive nbe_ty : ctx -> typ -> nf -> Prop := nbe_ty Γ M W ). #[export] -Hint Constructors nbe_ty : mcltt. +Hint Constructors nbe_ty : mctt. Lemma functional_nbe_ty : forall Γ M w w', nbe_ty Γ M w -> @@ -166,7 +166,7 @@ Proof. Qed. #[export] -Hint Resolve functional_nbe_ty nbe_type_to_nbe_ty : mcltt. +Hint Resolve functional_nbe_ty nbe_type_to_nbe_ty : mctt. Ltac functional_nbe_rewrite_clear1 := let tactic_error o1 o2 := fail 3 "functional_nbe equality between" o1 "and" o2 "cannot be solved by mauto" in diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v index 9e75694..dfecff0 100644 --- a/theories/Core/Semantic/PER.v +++ b/theories/Core/Semantic/PER.v @@ -1 +1 @@ -From Mcltt.Core.Semantic.PER Require Export CoreTactics Definitions Lemmas. +From Mctt.Core.Semantic.PER Require Export CoreTactics Definitions Lemmas. diff --git a/theories/Core/Semantic/PER/CoreTactics.v b/theories/Core/Semantic/PER/CoreTactics.v index 483f4cf..3ab431f 100644 --- a/theories/Core/Semantic/PER/CoreTactics.v +++ b/theories/Core/Semantic/PER/CoreTactics.v @@ -1,9 +1,9 @@ From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses. From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Import PER.Definitions. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Import PER.Definitions. Import Domain_Notations. Ltac destruct_rel_by_assumption in_rel H := diff --git a/theories/Core/Semantic/PER/Definitions.v b/theories/Core/Semantic/PER/Definitions.v index 4ba952f..bfae7a2 100644 --- a/theories/Core/Semantic/PER/Definitions.v +++ b/theories/Core/Semantic/PER/Definitions.v @@ -1,9 +1,9 @@ From Coq Require Import Lia PeanoNat Relation_Definitions RelationClasses. From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Export Domain Evaluation Readback. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.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). @@ -24,14 +24,14 @@ Variant rel_mod_eval (R : relation domain -> domain -> domain -> Prop) A ρ A' #[global] Arguments mk_rel_mod_eval {_ _ _ _ _ _}. #[export] -Hint Constructors rel_mod_eval : mcltt. +Hint Constructors rel_mod_eval : mctt. (** Related modulo application *) Variant rel_mod_app f a f' a' (R : relation domain) : Prop := mk_rel_mod_app : forall fa f'a', {{ $| f & a |↘ fa }} -> {{ $| f' & a' |↘ f'a' }} -> {{ Dom fa ≈ f'a' ∈ R }} -> rel_mod_app f a f' a' R. #[global] Arguments mk_rel_mod_app {_ _ _ _ _}. #[export] -Hint Constructors rel_mod_app : mcltt. +Hint Constructors rel_mod_app : mctt. (** *** (Some Elements of) PER Lattice *) @@ -39,25 +39,25 @@ Definition per_bot : relation domain_ne := fun m m' => (forall s, exists L, {{ R #[global] Arguments per_bot /. #[export] -Hint Transparent per_bot : mcltt. +Hint Transparent per_bot : mctt. #[export] -Hint Unfold per_bot : mcltt. +Hint Unfold per_bot : mctt. Definition per_top : relation domain_nf := fun m m' => (forall s, exists L, {{ Rnf m in s ↘ L }} /\ {{ Rnf m' in s ↘ L }}). #[global] Arguments per_top /. #[export] -Hint Transparent per_top : mcltt. +Hint Transparent per_top : mctt. #[export] -Hint Unfold per_top : mcltt. +Hint Unfold per_top : mctt. Definition per_top_typ : relation domain := fun a a' => (forall s, exists C, {{ Rtyp a in s ↘ C }} /\ {{ Rtyp a' in s ↘ C }}). #[global] Arguments per_top_typ /. #[export] -Hint Transparent per_top_typ : mcltt. +Hint Transparent per_top_typ : mctt. #[export] -Hint Unfold per_top_typ : mcltt. +Hint Unfold per_top_typ : mctt. Inductive per_nat : relation domain := | per_nat_zero : {{ Dom zero ≈ zero ∈ per_nat }} @@ -69,7 +69,7 @@ Inductive per_nat : relation domain := {{ Dom ⇑ a m ≈ ⇑ a' m' ∈ per_nat }} } . #[export] -Hint Constructors per_nat : mcltt. +Hint Constructors per_nat : mctt. Variant per_eq (point_rel : relation domain) m1 m2' : relation domain := | per_eq_refl : @@ -82,7 +82,7 @@ Variant per_eq (point_rel : relation domain) m1 m2' : relation domain := {{ Dom ⇑ a n ≈ ⇑ a' n' ∈ per_eq point_rel m1 m2' }} } . #[export] -Hint Constructors per_eq : mcltt. +Hint Constructors per_eq : mctt. Variant per_ne : relation domain := | per_ne_neut : @@ -90,7 +90,7 @@ Variant per_ne : relation domain := {{ Dom ⇑ a m ≈ ⇑ a' m' ∈ per_ne }} } . #[export] -Hint Constructors per_ne : mcltt. +Hint Constructors per_ne : mctt. (** * Universe/Element PER *) (** ** Universe/Element PER Definition *) @@ -187,7 +187,7 @@ Section Per_univ_elem_core_def. End Per_univ_elem_core_def. #[export] -Hint Constructors per_univ_elem_core : mcltt. +Hint Constructors per_univ_elem_core : mctt. Equations per_univ_elem (i : nat) : relation domain -> domain -> domain -> Prop by wf i := | i => per_univ_elem_core i (fun j lt_j_i a a' => exists R', {{ DF a ≈ a' ∈ per_univ_elem j ↘ R' }}). @@ -196,9 +196,9 @@ Definition per_univ (i : nat) : relation domain := fun a a' => exists R', {{ DF #[global] Arguments per_univ _ _ _ /. #[export] -Hint Transparent per_univ : mcltt. +Hint Transparent per_univ : mctt. #[export] -Hint Unfold per_univ : mcltt. +Hint Unfold per_univ : mctt. Lemma per_univ_elem_core_univ' : forall j i elem_rel, j < i -> @@ -211,7 +211,7 @@ Proof. Qed. #[export] -Hint Resolve per_univ_elem_core_univ' : mcltt. +Hint Resolve per_univ_elem_core_univ' : mctt. (** ** Universe/Element PER Induction Principle *) @@ -302,14 +302,14 @@ Inductive per_subtyp : nat -> domain -> domain -> Prop := where "'Sub' a <: b 'at' i" := (per_subtyp i a b) (in custom judg) : type_scope. #[export] -Hint Constructors per_subtyp : mcltt. + Hint Constructors per_subtyp : mctt. Definition rel_typ i A ρ A' ρ' R' := rel_mod_eval (per_univ_elem i) A ρ A' ρ' R'. Arguments rel_typ _ _ _ _ _ _ /. #[export] -Hint Transparent rel_typ : mcltt. +Hint Transparent rel_typ : mctt. #[export] -Hint Unfold rel_typ : mcltt. +Hint Unfold rel_typ : mctt. (** * Context/Environment PER *) @@ -319,7 +319,7 @@ Variant cons_per_ctx_env tail_rel (head_rel : forall {ρ ρ'} (equiv_ρ_ρ' : {{ {{ Dom ^(ρ 0) ≈ ^(ρ' 0) ∈ head_rel equiv_ρ_drop_ρ'_drop }} -> {{ Dom ρ ≈ ρ' ∈ cons_per_ctx_env tail_rel (@head_rel) }} }. #[export] -Hint Constructors cons_per_ctx_env : mcltt. +Hint Constructors cons_per_ctx_env : mctt. Inductive per_ctx_env : relation env -> ctx -> ctx -> Prop := | per_ctx_env_nil : @@ -338,14 +338,14 @@ Inductive per_ctx_env : relation env -> ctx -> ctx -> Prop := {{ EF Γ, A ≈ Γ', A' ∈ per_ctx_env ↘ env_rel }} } . #[export] -Hint Constructors per_ctx_env : mcltt. +Hint Constructors per_ctx_env : mctt. Definition per_ctx : relation ctx := fun Γ Γ' => exists R', per_ctx_env R' Γ Γ'. Definition valid_ctx : ctx -> Prop := fun Γ => per_ctx Γ Γ. #[export] -Hint Transparent valid_ctx : mcltt. +Hint Transparent valid_ctx : mctt. #[export] -Hint Unfold valid_ctx : mcltt. +Hint Unfold valid_ctx : mctt. Reserved Notation "'SubE' Γ <: Δ" (in custom judg at level 90, Γ custom exp, Δ custom exp). @@ -369,4 +369,4 @@ Inductive per_ctx_subtyp : ctx -> ctx -> Prop := where "'SubE' Γ <: Δ" := (per_ctx_subtyp Γ Δ) (in custom judg) : type_scope. #[export] -Hint Constructors per_ctx_subtyp : mcltt. +Hint Constructors per_ctx_subtyp : mctt. diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v index 3a960a9..bf198d1 100644 --- a/theories/Core/Semantic/PER/Lemmas.v +++ b/theories/Core/Semantic/PER/Lemmas.v @@ -1,9 +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 LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Import PER.CoreTactics PER.Definitions. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.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' ρ') @@ -31,7 +31,7 @@ Proof with solve [eauto]. Qed. #[export] -Hint Resolve per_bot_sym : mcltt. +Hint Resolve per_bot_sym : mctt. Lemma per_bot_trans : forall m n l, {{ Dom m ≈ n ∈ per_bot }} -> @@ -45,7 +45,7 @@ Proof with solve [eauto]. Qed. #[export] -Hint Resolve per_bot_trans : mcltt. +Hint Resolve per_bot_trans : mctt. #[export] Instance per_bot_PER : PER per_bot. @@ -62,7 +62,7 @@ Proof. Qed. #[export] -Hint Resolve var_per_bot : mcltt. +Hint Resolve var_per_bot : mctt. Lemma per_top_sym : forall m n, {{ Dom m ≈ n ∈ per_top }} -> @@ -74,7 +74,7 @@ Proof with solve [eauto]. Qed. #[export] -Hint Resolve per_top_sym : mcltt. +Hint Resolve per_top_sym : mctt. Lemma per_top_trans : forall m n l, {{ Dom m ≈ n ∈ per_top }} -> @@ -88,7 +88,7 @@ Proof with solve [eauto]. Qed. #[export] -Hint Resolve per_top_trans : mcltt. +Hint Resolve per_top_trans : mctt. #[export] Instance per_top_PER : PER per_top. @@ -109,7 +109,7 @@ Proof. Qed. #[export] -Hint Resolve per_bot_then_per_top : mcltt. +Hint Resolve per_bot_then_per_top : mctt. Lemma per_top_typ_sym : forall m n, {{ Dom m ≈ n ∈ per_top_typ }} -> @@ -121,7 +121,7 @@ Proof with solve [eauto]. Qed. #[export] -Hint Resolve per_top_typ_sym : mcltt. +Hint Resolve per_top_typ_sym : mctt. Lemma per_top_typ_trans : forall m n l, {{ Dom m ≈ n ∈ per_top_typ }} -> @@ -135,7 +135,7 @@ Proof with solve [eauto]. Qed. #[export] -Hint Resolve per_top_typ_trans : mcltt. +Hint Resolve per_top_typ_trans : mctt. #[export] Instance per_top_typ_PER : PER per_top_typ. @@ -153,7 +153,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve per_nat_sym : mcltt. +Hint Resolve per_nat_sym : mctt. Lemma per_nat_trans : forall m n l, {{ Dom m ≈ n ∈ per_nat }} -> @@ -165,7 +165,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve per_nat_trans : mcltt. +Hint Resolve per_nat_trans : mctt. #[export] Instance per_nat_PER : PER per_nat. @@ -184,7 +184,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve per_eq_sym : mcltt. +Hint Resolve per_eq_sym : mctt. Lemma per_eq_trans : forall point_rel m1 m2 n n' n'', PER point_rel -> @@ -198,7 +198,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve per_eq_trans : mcltt. +Hint Resolve per_eq_trans : mctt. #[export] Instance per_eq_PER {point_rel m1 m2} {Hpoint : PER point_rel} : PER (per_eq point_rel m1 m2). @@ -271,7 +271,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve per_ne_sym : mcltt. +Hint Resolve per_ne_sym : mctt. Lemma per_ne_trans : forall m n l, {{ Dom m ≈ n ∈ per_ne }} -> @@ -284,7 +284,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve per_ne_trans : mcltt. +Hint Resolve per_ne_trans : mctt. #[export] Instance per_ne_PER : PER per_ne. @@ -676,7 +676,7 @@ Ltac per_univ_elem_econstructor := (repeat intro; hnf; (eapply per_univ_elem_pi' || eapply per_univ_elem_eq')) + basic_per_univ_elem_econstructor. #[export] -Hint Resolve per_univ_elem_pi' per_univ_elem_eq' : mcltt. +Hint Resolve per_univ_elem_pi' per_univ_elem_eq' : mctt. Lemma per_univ_elem_pi_clean_inversion : forall {i j a a' in_rel ρ ρ' B B' elem_rel}, {{ DF a ≈ a' ∈ per_univ_elem i ↘ in_rel }} -> @@ -732,7 +732,7 @@ Proof with solve [eauto]. Qed. #[export] -Hint Resolve per_univ_elem_cumu : mcltt. +Hint Resolve per_univ_elem_cumu : mctt. Lemma per_univ_elem_cumu_ge : forall i i' a0 a1 R, i <= i' -> @@ -743,7 +743,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve per_univ_elem_cumu_ge : mcltt. +Hint Resolve per_univ_elem_cumu_ge : mctt. Lemma per_univ_elem_cumu_max_left : forall i j a0 a1 R, {{ DF a0 ≈ a1 ∈ per_univ_elem i ↘ R }} -> @@ -832,7 +832,7 @@ Proof. Qed. #[export] -Hint Resolve per_subtyp_refl1 : mcltt. +Hint Resolve per_subtyp_refl1 : mctt. Lemma per_subtyp_refl2 : forall a b i R, {{ DF a ≈ b ∈ per_univ_elem i ↘ R }} -> @@ -844,7 +844,7 @@ Proof. Qed. #[export] -Hint Resolve per_subtyp_refl2 : mcltt. +Hint Resolve per_subtyp_refl2 : mctt. Lemma per_subtyp_trans : forall a1 a2 i, {{ Sub a1 <: a2 at i }} -> @@ -871,7 +871,7 @@ Proof. Qed. #[export] -Hint Resolve per_subtyp_trans : mcltt. +Hint Resolve per_subtyp_trans : mctt. #[export] Instance per_subtyp_trans_ins i : Transitive (per_subtyp i). @@ -899,7 +899,7 @@ Proof. Qed. #[export] -Hint Resolve per_subtyp_cumu : mcltt. +Hint Resolve per_subtyp_cumu : mctt. Lemma per_subtyp_cumu_left : forall a1 a2 i j, {{ Sub a1 <: a2 at i }} -> @@ -1138,7 +1138,7 @@ Proof. Qed. #[export] -Hint Resolve per_ctx_env_cons' : mcltt. +Hint Resolve per_ctx_env_cons' : mctt. Ltac per_ctx_env_econstructor := (repeat intro; hnf; eapply per_ctx_env_cons') + econstructor. @@ -1284,7 +1284,7 @@ Proof. Qed. #[export] -Hint Resolve per_ctx_subtyp_trans : mcltt. +Hint Resolve per_ctx_subtyp_trans : mctt. #[export] Instance per_ctx_subtyp_trans_ins : Transitive per_ctx_subtyp. diff --git a/theories/Core/Semantic/Readback.v b/theories/Core/Semantic/Readback.v index 41c3ac3..b159275 100644 --- a/theories/Core/Semantic/Readback.v +++ b/theories/Core/Semantic/Readback.v @@ -1 +1 @@ -From Mcltt.Core.Semantic.Readback Require Export Definitions Lemmas. +From Mctt.Core.Semantic.Readback Require Export Definitions Lemmas. diff --git a/theories/Core/Semantic/Readback/Definitions.v b/theories/Core/Semantic/Readback/Definitions.v index 53dde90..25c18a3 100644 --- a/theories/Core/Semantic/Readback/Definitions.v +++ b/theories/Core/Semantic/Readback/Definitions.v @@ -1,6 +1,6 @@ -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Import Evaluation. -From Mcltt.Core.Semantic Require Export Domain. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Import Evaluation. +From Mctt.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). @@ -126,4 +126,4 @@ Combined Scheme read_mut_ind from read_typ_mut_ind. #[export] -Hint Constructors read_nf read_ne read_typ : mcltt. +Hint Constructors read_nf read_ne read_typ : mctt. diff --git a/theories/Core/Semantic/Readback/Lemmas.v b/theories/Core/Semantic/Readback/Lemmas.v index 52d53bb..769a848 100644 --- a/theories/Core/Semantic/Readback/Lemmas.v +++ b/theories/Core/Semantic/Readback/Lemmas.v @@ -1,9 +1,9 @@ From Coq Require Import Lia PeanoNat Relations. -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. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Import Evaluation. +From Mctt.Core.Semantic.Readback Require Import Definitions. Import Domain_Notations. Section functional_read. @@ -53,7 +53,7 @@ Section functional_read. End functional_read. #[export] -Hint Resolve functional_read_nf functional_read_ne functional_read_typ : mcltt. +Hint Resolve functional_read_nf functional_read_ne functional_read_typ : mctt. Ltac functional_read_rewrite_clear1 := let tactic_error o1 o2 := fail 3 "functional_read equality between" o1 "and" o2 "cannot be solved by mauto" in diff --git a/theories/Core/Semantic/Realizability.v b/theories/Core/Semantic/Realizability.v index 10134bb..20516a6 100644 --- a/theories/Core/Semantic/Realizability.v +++ b/theories/Core/Semantic/Realizability.v @@ -1,9 +1,9 @@ From Coq Require Import Lia Morphisms_Relations PeanoNat Relation_Definitions. From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Export NbE PER. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Export NbE PER. Import Domain_Notations. Lemma per_nat_then_per_top : forall {n m}, @@ -16,7 +16,7 @@ Proof with solve [destruct_conjs; eexists; repeat econstructor; eauto]. Qed. #[export] -Hint Resolve per_nat_then_per_top : mcltt. +Hint Resolve per_nat_then_per_top : mctt. Lemma realize_per_univ_elem_gen : forall {i a a' R}, {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} -> @@ -95,7 +95,7 @@ Proof. Qed. #[export] -Hint Resolve per_univ_then_per_top_typ : mcltt. +Hint Resolve per_univ_then_per_top_typ : mctt. Corollary per_bot_then_per_elem : forall {i a a' R c c'}, {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} -> @@ -116,7 +116,7 @@ Proof. Qed. #[export] -Hint Resolve per_elem_then_per_top : mcltt. +Hint Resolve per_elem_then_per_top : mctt. Lemma per_ctx_then_per_env_initial_env : forall {Γ Γ' env_rel}, {{ EF Γ ≈ Γ' ∈ per_ctx_env ↘ env_rel }} -> diff --git a/theories/Core/Soundness.v b/theories/Core/Soundness.v index b60bc9c..36f0e8f 100644 --- a/theories/Core/Soundness.v +++ b/theories/Core/Soundness.v @@ -1,9 +1,9 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import FundamentalTheorem. -From Mcltt.Core.Semantic Require Import Realizability. -From Mcltt.Core.Semantic Require Export NbE. -From Mcltt.Core.Soundness Require Export FundamentalTheorem. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import FundamentalTheorem. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Semantic Require Export NbE. +From Mctt.Core.Soundness Require Export FundamentalTheorem. Import Domain_Notations. Theorem soundness : forall {Γ M A}, diff --git a/theories/Core/Soundness/ContextCases.v b/theories/Core/Soundness/ContextCases.v index ad7c1dc..dc25c3f 100644 --- a/theories/Core/Soundness/ContextCases.v +++ b/theories/Core/Soundness/ContextCases.v @@ -1,6 +1,6 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Soundness Require Import LogicalRelation. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Soundness Require Import LogicalRelation. Import Domain_Notations. Lemma glu_rel_ctx_empty : {{ ⊩ ⋅ }}. @@ -9,7 +9,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_ctx_empty : mcltt. +Hint Resolve glu_rel_ctx_empty : mctt. Lemma glu_rel_ctx_extend : forall {Γ A i}, {{ ⊩ Γ }} -> @@ -24,4 +24,4 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_ctx_extend : mcltt. +Hint Resolve glu_rel_ctx_extend : mctt. diff --git a/theories/Core/Soundness/FunctionCases.v b/theories/Core/Soundness/FunctionCases.v index f7cbc11..bc52ac9 100644 --- a/theories/Core/Soundness/FunctionCases.v +++ b/theories/Core/Soundness/FunctionCases.v @@ -1,7 +1,7 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import FundamentalTheorem UniverseCases. -From Mcltt.Core.Soundness Require Import +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import FundamentalTheorem UniverseCases. +From Mctt.Core.Soundness Require Import ContextCases LogicalRelation SubstitutionCases @@ -29,7 +29,7 @@ Proof. Qed. #[local] -Hint Resolve cons_glu_sub_pred_pi_helper : mcltt. +Hint Resolve cons_glu_sub_pred_pi_helper : mctt. Lemma glu_rel_exp_pi : forall {Γ A B i}, {{ Γ ⊩ A : Type@i }} -> @@ -78,7 +78,7 @@ Proof. unfold univ_glu_exp_pred' in *. destruct_conjs. handle_functional_glu_univ_elem. - autorewrite with mcltt. + autorewrite with mctt. eassumption. - assert {{ Dom ρ ↦ m ≈ ρ ↦ m ∈ env_relΓA }} as HrelΓA by (apply_relation_equivalence; mautosolve 2). apply_relation_equivalence. @@ -104,7 +104,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_pi : mcltt. +Hint Resolve glu_rel_exp_pi : mctt. Lemma glu_rel_exp_of_pi : forall {Γ M A B i Sb}, {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> @@ -247,7 +247,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_fn : mcltt. +Hint Resolve glu_rel_exp_fn : mctt. Lemma glu_rel_exp_app_helper : forall {Γ M N A B i}, {{ Γ ⊩ A : Type@i }} -> @@ -316,7 +316,7 @@ Proof. assert (exists mn : domain, {{ $| m & n |↘ mn }} /\ {{ Δ ⊢ M[σ][Id] N[σ] : OT[Id,,N[σ]] ® mn ∈ OEl n equiv_n }}) as [] by mauto 2. destruct_conjs. functional_eval_rewrite_clear. - assert {{ Δ ⊢ N[σ] : A[σ][Id] ® n ∈ Ela }} by (autorewrite with mcltt; eassumption). + assert {{ Δ ⊢ N[σ] : A[σ][Id] ® n ∈ Ela }} by (autorewrite with mctt; eassumption). assert {{ Δ ⊢s σ∘Id,,N[σ] ® ρ ↦ n ∈ SbΓA }} as Hcons by (unfold SbΓA; mauto 2). (on_all_hyp: destruct_glu_rel_by_assumption SbΓA). simplify_evals. @@ -334,7 +334,7 @@ Proof. assert {{ Δ ⊢ M[σ][Id] ≈ M[σ] : (Π A B)[σ] }} by mauto 2. assert {{ Δ ⊢ M[σ][Id] ≈ M[σ] : Π A[σ] B[q σ] }} by mauto 3. assert {{ Δ ⊢ M[σ][Id] N[σ] ≈ M[σ] N[σ] : B[q σ][Id,,N[σ]] }} as HGoal' by mauto 3. - autorewrite with mcltt in HGoal'. + autorewrite with mctt in HGoal'. eassumption. } assert {{ Δ ⊢ B[σ,,N[σ]] ≈ B[(σ∘Id),,N[σ]] : Type@i }} as -> @@ -373,4 +373,4 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_app : mcltt. +Hint Resolve glu_rel_exp_app : mctt. diff --git a/theories/Core/Soundness/FundamentalTheorem.v b/theories/Core/Soundness/FundamentalTheorem.v index 3deb9ee..593cf73 100644 --- a/theories/Core/Soundness/FundamentalTheorem.v +++ b/theories/Core/Soundness/FundamentalTheorem.v @@ -1,6 +1,6 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Soundness Require Import +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Soundness Require Import ContextCases FunctionCases NatCases @@ -8,7 +8,7 @@ From Mcltt.Core.Soundness Require Import SubtypingCases TermStructureCases UniverseCases. -From Mcltt.Core.Soundness Require Export LogicalRelation. +From Mctt.Core.Soundness Require Export LogicalRelation. Import Domain_Notations. Section soundness_fundamental. diff --git a/theories/Core/Soundness/LogicalRelation.v b/theories/Core/Soundness/LogicalRelation.v index 5665881..eeef4ae 100644 --- a/theories/Core/Soundness/LogicalRelation.v +++ b/theories/Core/Soundness/LogicalRelation.v @@ -1 +1 @@ -From Mcltt.Core.Soundness.LogicalRelation Require Export Core Lemmas. +From Mctt.Core.Soundness.LogicalRelation Require Export Core Lemmas. diff --git a/theories/Core/Soundness/LogicalRelation/Core.v b/theories/Core/Soundness/LogicalRelation/Core.v index 6756fab..f72c761 100644 --- a/theories/Core/Soundness/LogicalRelation/Core.v +++ b/theories/Core/Soundness/LogicalRelation/Core.v @@ -1 +1 @@ -From Mcltt.Core.Soundness.LogicalRelation Require Export CoreLemmas CoreTactics Definitions. +From Mctt.Core.Soundness.LogicalRelation Require Export CoreLemmas CoreTactics Definitions. diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v index cd4bf38..0af7310 100644 --- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v +++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v @@ -1,9 +1,9 @@ From Coq Require Import Equivalence Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Soundness.LogicalRelation Require Import CoreTactics Definitions. -From Mcltt.Core.Soundness.Weakening Require Export Lemmas. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Soundness.LogicalRelation Require Import CoreTactics Definitions. +From Mctt.Core.Soundness.Weakening Require Export Lemmas. Import Domain_Notations. Lemma glu_nat_per_nat : forall Γ M a, @@ -14,7 +14,7 @@ Proof. Qed. #[local] -Hint Resolve glu_nat_per_nat : mcltt. +Hint Resolve glu_nat_per_nat : mctt. Lemma glu_nat_escape : forall Γ M a, glu_nat Γ M a -> @@ -34,7 +34,7 @@ Proof. Qed. #[export] -Hint Resolve glu_nat_escape : mcltt. +Hint Resolve glu_nat_escape : mctt. Lemma glu_nat_resp_ctx_eq : forall Γ M a Δ, glu_nat Γ M a -> @@ -45,7 +45,7 @@ Proof. Qed. #[local] -Hint Resolve glu_nat_resp_ctx_eq : mcltt. +Hint Resolve glu_nat_resp_ctx_eq : mctt. Add Parametric Morphism : glu_nat with signature wf_ctx_eq ==> eq ==> eq ==> iff as glu_ctx_env_sub_morphism_iff1. @@ -66,7 +66,7 @@ Proof. Qed. #[local] -Hint Resolve glu_nat_resp_exp_eq : mcltt. +Hint Resolve glu_nat_resp_exp_eq : mctt. Add Parametric Morphism Γ : (glu_nat Γ) with signature wf_exp_eq Γ {{{ ℕ }}} ==> eq ==> iff as glu_ctx_env_sub_morphism_iff2. @@ -241,7 +241,7 @@ Proof. Qed. #[export] -Hint Resolve glu_nat_resp_wk : mcltt. +Hint Resolve glu_nat_resp_wk : mctt. Lemma glu_univ_elem_trm_escape : forall i P El a, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> @@ -269,7 +269,7 @@ Proof. Qed. #[export] -Hint Resolve glu_univ_elem_per_univ : mcltt. +Hint Resolve glu_univ_elem_per_univ : mctt. Lemma glu_univ_elem_per_elem : forall i P El a, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> @@ -350,9 +350,9 @@ Proof. assert {{ Γ ⊢ M ≈ M' : Π IT OT }} as Hty by mauto. eassert {{ Δ ⊢ IT[σ] : Type@_ }} by mauto 3. eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [| eapply sub_eq_refl; mauto 3]. - autorewrite with mcltt in Hty. + autorewrite with mctt in Hty. eapply wf_exp_eq_app_cong with (N := N) (N' := N) in Hty; try pi_univ_level_tac; [|mauto 2]. - autorewrite with mcltt in Hty. + autorewrite with mctt in Hty. eassumption. - econstructor; eauto. destruct_glu_eq; econstructor; mauto 3. @@ -381,7 +381,7 @@ Proof. Qed. #[export] -Hint Resolve glu_univ_elem_core_univ' : mcltt. +Hint Resolve glu_univ_elem_core_univ' : mctt. Ltac glu_univ_elem_econstructor := eapply glu_univ_elem_core_univ' + basic_glu_univ_elem_econstructor. @@ -394,7 +394,7 @@ Proof. Qed. #[export] -Hint Resolve glu_univ_elem_univ_simple_constructor : mcltt. +Hint Resolve glu_univ_elem_univ_simple_constructor : mctt. Ltac rewrite_predicate_equivalence_left := repeat match goal with @@ -679,7 +679,7 @@ Proof. Qed. #[local] - Hint Resolve glu_nat_resp_per_nat : mcltt. + Hint Resolve glu_nat_resp_per_nat : mctt. #[local] Ltac resp_per_IH := @@ -900,7 +900,7 @@ Proof. Qed. #[export] -Hint Resolve per_univ_glu_univ_elem : mcltt. +Hint Resolve per_univ_glu_univ_elem : mctt. Corollary per_univ_elem_glu_univ_elem : forall i a R, {{ DF a ≈ a ∈ per_univ_elem i ↘ R }} -> @@ -911,7 +911,7 @@ Proof. Qed. #[export] -Hint Resolve per_univ_elem_glu_univ_elem : mcltt. +Hint Resolve per_univ_elem_glu_univ_elem : mctt. Ltac saturate_glu_info1 := match goal with @@ -930,8 +930,7 @@ Ltac saturate_glu_info := repeat saturate_glu_info1. #[local] -Hint Rewrite -> sub_decompose_q using solve [mauto 4] : mcltt. - +Hint Rewrite -> sub_decompose_q using solve [mauto 4] : mctt. Lemma glu_univ_elem_mut_monotone : forall i a P El, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> @@ -966,7 +965,7 @@ Proof. destruct_rel_mod_eval. simplify_evals. deepexec H1 ltac:(fun H => pose proof H). - autorewrite with mcltt in *. + autorewrite with mctt in *. mauto 3. - simpl_glu_rel. @@ -981,7 +980,7 @@ Proof. destruct_rel_mod_app. simplify_evals. deepexec H1 ltac:(fun H => pose proof H). - autorewrite with mcltt in *. + autorewrite with mctt in *. repeat eexists; eauto. assert {{ Δ0 ⊢s σ0,,N : Δ, IT[σ] }}. { @@ -1044,15 +1043,15 @@ Proof. split; [mauto 3 |]. intros. saturate_weakening_escape. - autorewrite with mcltt. + autorewrite with mctt. mauto 3. - simpl_glu_rel. econstructor; repeat split; mauto 3; intros; saturate_weakening_escape. - + autorewrite with mcltt. + + autorewrite with mctt. mauto 3. - + autorewrite with mcltt. + + autorewrite with mctt. etransitivity. * symmetry. eapply wf_exp_eq_sub_compose; diff --git a/theories/Core/Soundness/LogicalRelation/CoreTactics.v b/theories/Core/Soundness/LogicalRelation/CoreTactics.v index 551f2c2..411b371 100644 --- a/theories/Core/Soundness/LogicalRelation/CoreTactics.v +++ b/theories/Core/Soundness/LogicalRelation/CoreTactics.v @@ -1,8 +1,8 @@ From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Soundness.LogicalRelation Require Import Definitions. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Soundness.LogicalRelation Require Import Definitions. Ltac basic_invert_glu_univ_elem H := progress simp glu_univ_elem in H; diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v index 88f46be..42284b3 100644 --- a/theories/Core/Soundness/LogicalRelation/Definitions.v +++ b/theories/Core/Soundness/LogicalRelation/Definitions.v @@ -1,10 +1,10 @@ From Coq Require Import Relation_Definitions RelationClasses. From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Export PER. -From Mcltt.Core.Soundness.Weakening Require Export Definitions. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Export PER. +From Mctt.Core.Soundness.Weakening Require Export Definitions. Import Domain_Notations. Global Open Scope predicate_scope. @@ -44,7 +44,7 @@ Inductive glu_nat : ctx -> exp -> domain -> Prop := glu_nat Γ M d{{{ ⇑ a m }}} }. #[export] -Hint Constructors glu_nat : mcltt. +Hint Constructors glu_nat : mctt. Definition nat_glu_typ_pred i : glu_typ_pred := fun Γ A => {{ Γ ⊢ A ≈ ℕ : Type@i }}. Arguments nat_glu_typ_pred i Γ A/. @@ -150,7 +150,7 @@ Variant eq_glu_exp_pred i m n R P El : glu_exp_pred := pi_glu_typ_pred pi_glu_exp_pred eq_glu_typ_pred - glu_eq eq_glu_exp_pred : mcltt. + glu_eq eq_glu_exp_pred : mctt. Definition univ_glu_typ_pred j i : glu_typ_pred := fun Γ A => {{ Γ ⊢ A ≈ Type@j : Type@i }}. Arguments univ_glu_typ_pred j i Γ A/. @@ -221,7 +221,7 @@ Section Gluing. End Gluing. #[export] -Hint Constructors glu_univ_elem_core : mcltt. +Hint Constructors glu_univ_elem_core : mctt. Equations glu_univ_elem (i : nat) : glu_typ_pred -> glu_exp_pred -> domain -> Prop by wf i := | i => glu_univ_elem_core i (fun j lt_j_i a Γ A => exists P El, {{ DG a ∈ glu_univ_elem j ↘ P ↘ El }} /\ {{ Γ ⊢ A ® P }}). @@ -333,7 +333,7 @@ Variant glu_elem_bot i a Γ A M m : Prop := (forall Δ σ M', {{ Δ ⊢w σ : Γ }} -> {{ Rne m in length Δ ↘ M' }} -> {{ Δ ⊢ M[σ] ≈ M' : A[σ] }}) -> {{ Γ ⊢ M : A ® m ∈ glu_elem_bot i a }}. #[export] -Hint Constructors glu_elem_bot : mcltt. +Hint Constructors glu_elem_bot : mctt. Variant glu_elem_top i a Γ A M m : Prop := | glu_elem_top_make : forall P El, @@ -344,7 +344,7 @@ Variant glu_elem_top i a Γ A M m : Prop := (forall Δ σ w, {{ Δ ⊢w σ : Γ }} -> {{ Rnf ⇓ a m in length Δ ↘ w }} -> {{ Δ ⊢ M[σ] ≈ w : A[σ] }}) -> {{ Γ ⊢ M : A ® m ∈ glu_elem_top i a }}. #[export] -Hint Constructors glu_elem_top : mcltt. +Hint Constructors glu_elem_top : mctt. Variant glu_typ_top i a Γ A : Prop := | glu_typ_top_make : @@ -353,7 +353,7 @@ Variant glu_typ_top i a Γ A : Prop := (forall Δ σ A', {{ Δ ⊢w σ : Γ }} -> {{ Rtyp a in length Δ ↘ A' }} -> {{ Δ ⊢ A[σ] ≈ A' : Type@i }}) -> {{ Γ ⊢ A ® glu_typ_top i a }}. #[export] -Hint Constructors glu_typ_top : mcltt. +Hint Constructors glu_typ_top : mctt. Variant glu_rel_typ_with_sub i Δ A σ ρ : Prop := | mk_glu_rel_typ_with_sub : diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v index 6b10196..da0649f 100644 --- a/theories/Core/Soundness/LogicalRelation/Lemmas.v +++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v @@ -1,10 +1,10 @@ From Coq Require Import Equivalence Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import FundamentalTheorem. -From Mcltt.Core.Semantic Require Import Realizability. -From Mcltt.Core.Soundness Require Export Realizability. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import FundamentalTheorem. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Soundness Require Export Realizability. Import Domain_Notations. Add Parametric Morphism i a Γ A M : (glu_elem_bot i a Γ A M) @@ -51,11 +51,11 @@ Proof with mautosolve 4. assert {{ Γ ⊢ A[Id] ≈ V : Type@(max i j) }} by mauto 4 using lift_exp_eq_max_left. assert {{ Γ ⊢ A'[Id] ≈ V : Type@j }} by mauto 4. assert {{ Γ ⊢ A'[Id] ≈ V : Type@(max i j) }} by mauto 4 using lift_exp_eq_max_right. - autorewrite with mcltt in *... + autorewrite with mctt in *... Qed. #[export] -Hint Resolve glu_univ_elem_typ_unique_upto_exp_eq : mcltt. +Hint Resolve glu_univ_elem_typ_unique_upto_exp_eq : mctt. Lemma glu_univ_elem_typ_unique_upto_exp_eq_ge : forall {i j a P P' El El' Γ A A'}, i <= j -> @@ -70,7 +70,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve glu_univ_elem_typ_unique_upto_exp_eq_ge : mcltt. +Hint Resolve glu_univ_elem_typ_unique_upto_exp_eq_ge : mctt. Lemma glu_univ_elem_typ_unique_upto_exp_eq' : forall {i a P El Γ A A'}, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> @@ -80,7 +80,7 @@ Lemma glu_univ_elem_typ_unique_upto_exp_eq' : forall {i a P El Γ A A'}, Proof. mautosolve 4. Qed. #[export] -Hint Resolve glu_univ_elem_typ_unique_upto_exp_eq' : mcltt. +Hint Resolve glu_univ_elem_typ_unique_upto_exp_eq' : mctt. Lemma glu_univ_elem_per_univ_elem_typ_escape : forall {i a a' elem_rel P P' El El' Γ A A'}, {{ DF a ≈ a' ∈ per_univ_elem i ↘ elem_rel }} -> @@ -97,7 +97,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve glu_univ_elem_per_univ_elem_typ_escape : mcltt. +Hint Resolve glu_univ_elem_per_univ_elem_typ_escape : mctt. Lemma glu_univ_elem_per_univ_typ_escape : forall {i a a' P P' El El' Γ A A'}, {{ Dom a ≈ a' ∈ per_univ i }} -> @@ -112,7 +112,7 @@ Proof. Qed. #[export] -Hint Resolve glu_univ_elem_per_univ_typ_escape : mcltt. +Hint Resolve glu_univ_elem_per_univ_typ_escape : mctt. Lemma glu_univ_elem_per_univ_typ_iff : forall {i a a' P P' El El'}, {{ Dom a ≈ a' ∈ per_univ i }} -> @@ -138,7 +138,7 @@ Proof. Qed. #[export] -Hint Resolve glu_univ_elem_cumu_ge : mcltt. +Hint Resolve glu_univ_elem_cumu_ge : mctt. Corollary glu_univ_elem_cumu_max_left : forall {i j a P El}, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> @@ -415,13 +415,13 @@ Proof. { assert {{ Γ ⊢ IT[Id] ® IP }} by mauto 4. simpl in *. - autorewrite with mcltt in *; mauto 3. + autorewrite with mctt in *; mauto 3. } assert {{ Γ ⊢ IT' ® IP }}. { assert {{ Γ ⊢ IT'[Id] ® IP }} by mauto 4. simpl in *. - autorewrite with mcltt in *; mauto 3. + autorewrite with mctt in *; mauto 3. } do 2 bulky_rewrite1. assert {{ Γ ⊢ IT ≈ IT' : Type@i }} by mauto 4. @@ -460,7 +460,7 @@ Proof. Qed. #[export] -Hint Resolve glu_univ_elem_per_subtyp_typ_escape : mcltt. +Hint Resolve glu_univ_elem_per_subtyp_typ_escape : mctt. Lemma glu_univ_elem_per_subtyp_trm_if : forall {i a a' P P' El El' Γ A A' M m}, {{ Sub a <: a' at i }} -> @@ -514,13 +514,13 @@ Proof. { assert {{ Γ ⊢ IT[Id] ® IP }} by mauto 3. simpl in *. - autorewrite with mcltt in *; mauto 3. + autorewrite with mctt in *; mauto 3. } assert {{ Γ ⊢ IT' ® IP }}. { assert {{ Γ ⊢ IT'[Id] ® IP }} by mauto 3. simpl in *. - autorewrite with mcltt in *; mauto 3. + autorewrite with mctt in *; mauto 3. } assert {{ Δ ⊢ IT'[σ] ≈ IT[σ] : Type@i }} by (symmetry; mauto 4 using glu_univ_elem_per_univ_typ_escape). assert {{ Δ ⊢ N : IT'[σ] ® n ∈ IEl }} by (simpl; bulky_rewrite1; eassumption). @@ -578,7 +578,7 @@ Proof. Qed. #[export] -Hint Resolve mk_glu_rel_typ_with_sub' : mcltt. +Hint Resolve mk_glu_rel_typ_with_sub' : mctt. Lemma mk_glu_rel_typ_with_sub'' : forall {i Δ A σ ρ a}, {{ ⟦ A ⟧ ρ ↘ a }} -> @@ -592,7 +592,7 @@ Proof. Qed. #[export] -Hint Resolve mk_glu_rel_typ_with_sub'' : mcltt. +Hint Resolve mk_glu_rel_typ_with_sub'' : mctt. Lemma mk_glu_rel_exp_with_sub' : forall {i Δ A M σ ρ a m}, {{ ⟦ A ⟧ ρ ↘ a }} -> @@ -607,7 +607,7 @@ Proof. Qed. #[export] -Hint Resolve mk_glu_rel_exp_with_sub' : mcltt. +Hint Resolve mk_glu_rel_exp_with_sub' : mctt. Lemma mk_glu_rel_exp_with_sub'' : forall {i Δ A M σ ρ a m}, {{ ⟦ A ⟧ ρ ↘ a }} -> @@ -622,7 +622,7 @@ Proof. Qed. #[export] -Hint Resolve mk_glu_rel_exp_with_sub'' : mcltt. +Hint Resolve mk_glu_rel_exp_with_sub'' : mctt. Lemma glu_rel_exp_with_sub_implies_glu_rel_exp_sub_with_typ : forall {i Δ A M σ Γ ρ}, {{ Δ ⊢s σ : Γ }} -> @@ -638,7 +638,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_with_sub_implies_glu_rel_exp_sub_with_typ : mcltt. +Hint Resolve glu_rel_exp_with_sub_implies_glu_rel_exp_sub_with_typ : mctt. Lemma glu_rel_exp_with_sub_implies_glu_rel_typ_with_sub : forall {i Δ A j σ ρ}, glu_rel_exp_with_sub i Δ A {{{ Type@j }}} σ ρ -> @@ -654,7 +654,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_with_sub_implies_glu_rel_typ_with_sub : mcltt. +Hint Resolve glu_rel_exp_with_sub_implies_glu_rel_typ_with_sub : mctt. Lemma glu_rel_typ_with_sub_implies_glu_rel_exp_with_sub : forall {Δ A j σ Γ ρ}, {{ Δ ⊢s σ : Γ }} -> @@ -669,7 +669,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_typ_with_sub_implies_glu_rel_exp_with_sub : mcltt. +Hint Resolve glu_rel_typ_with_sub_implies_glu_rel_exp_with_sub : mctt. (** *** Lemmas for [glu_ctx_env] *) @@ -793,7 +793,7 @@ Proof. Qed. #[export] -Hint Resolve glu_ctx_env_wf_ctx glu_ctx_env_sub_escape : mcltt. +Hint Resolve glu_ctx_env_wf_ctx glu_ctx_env_sub_escape : mctt. Lemma glu_ctx_env_per_ctx_env : forall {Γ Sb}, {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> @@ -805,7 +805,7 @@ Proof. Qed. #[export] -Hint Resolve glu_ctx_env_per_ctx_env : mcltt. +Hint Resolve glu_ctx_env_per_ctx_env : mctt. Lemma glu_ctx_env_resp_per_ctx_helper : forall {Γ Γ' Sb Sb'}, {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> @@ -855,7 +855,7 @@ Proof. eapply glu_univ_elem_exp_cumu_ge; mauto 3. } eapply glu_univ_elem_exp_conv; [eexists | | | |]; intuition. - autorewrite with mcltt. + autorewrite with mctt. eassumption. Qed. @@ -953,7 +953,7 @@ Proof. destruct_by_head rel_exp. handle_functional_glu_ctx_env. eapply glu_univ_elem_per_subtyp_trm_conv; mauto 3. - autorewrite with mcltt. + autorewrite with mctt. eassumption. Qed. @@ -998,13 +998,13 @@ Proof. assert {{ Δ ⊢ M : A[σ] }} by mauto 2 using glu_univ_elem_trm_escape. assert {{ Δ ⊢s σ,,M : Γ, A }} by mauto 2. econstructor; mauto 3; - autorewrite with mcltt; mauto 3. + autorewrite with mctt; mauto 3. assert {{ Δ ⊢ #0[σ,,M] ≈ M : A[σ] }} as ->; mauto 2. Qed. #[export] -Hint Resolve cons_glu_sub_pred_helper : mcltt. +Hint Resolve cons_glu_sub_pred_helper : mctt. Lemma initial_env_glu_rel_exp : forall {Γ ρ Sb}, initial_env Γ ρ -> @@ -1145,7 +1145,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_to_wf_exp : mcltt. +Hint Resolve glu_rel_exp_to_wf_exp : mctt. (** *** Lemmas about [glu_rel_sub] *) @@ -1220,4 +1220,4 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_sub_wf_sub : mcltt. +Hint Resolve glu_rel_sub_wf_sub : mctt. diff --git a/theories/Core/Soundness/NatCases.v b/theories/Core/Soundness/NatCases.v index 00c0b93..3d3f306 100644 --- a/theories/Core/Soundness/NatCases.v +++ b/theories/Core/Soundness/NatCases.v @@ -1,8 +1,8 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import FundamentalTheorem. -From Mcltt.Core.Semantic Require Import Realizability. -From Mcltt.Core.Soundness Require Import +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import FundamentalTheorem. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Soundness Require Import ContextCases LogicalRelation SubstitutionCases @@ -31,7 +31,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_nat : mcltt. +Hint Resolve glu_rel_exp_nat : mctt. Lemma glu_rel_exp_sub_nat : forall {Γ σ Δ M}, {{ Γ ⊩s σ : Δ }} -> @@ -46,7 +46,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_sub_nat : mcltt. +Hint Resolve glu_rel_exp_sub_nat : mctt. Lemma glu_rel_exp_clean_inversion2'' : forall {Γ Sb M}, {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> @@ -95,7 +95,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_zero : mcltt. +Hint Resolve glu_rel_exp_zero : mctt. Lemma glu_rel_exp_succ : forall {Γ M}, {{ Γ ⊩ M : ℕ }} -> @@ -117,7 +117,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_succ : mcltt. +Hint Resolve glu_rel_exp_succ : mctt. Lemma glu_rel_sub_extend_nat : forall {Γ σ Δ M}, {{ Γ ⊩s σ : Δ }} -> @@ -133,7 +133,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_sub_extend_nat : mcltt. +Hint Resolve glu_rel_sub_extend_nat : mctt. Lemma glu_rel_exp_natrec_zero_helper : forall {i Γ SbΓ A MZ MS Δ M σ ρ am P El}, {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} -> @@ -202,7 +202,7 @@ Proof. Qed. #[local] -Hint Resolve cons_glu_sub_pred_nat_helper : mcltt. +Hint Resolve cons_glu_sub_pred_nat_helper : mctt. Lemma glu_rel_exp_natrec_succ_helper : forall {i Γ SbΓ A MZ MS Δ M M' m' σ ρ am P El}, {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} -> @@ -328,7 +328,7 @@ Proof. Qed. #[local] -Hint Resolve cons_glu_sub_pred_q_helper : mcltt. +Hint Resolve cons_glu_sub_pred_q_helper : mctt. Lemma cons_glu_sub_pred_q_nat_helper : forall {Γ SbΓ Δ σ ρ i}, {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} -> @@ -350,7 +350,7 @@ Proof. Qed. #[local] -Hint Resolve cons_glu_sub_pred_q_nat_helper : mcltt. +Hint Resolve cons_glu_sub_pred_q_nat_helper : mctt. Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M a m σ ρ am P El}, {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} -> @@ -673,4 +673,4 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_natrec : mcltt. +Hint Resolve glu_rel_exp_natrec : mctt. diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v index a928e21..58884c5 100644 --- a/theories/Core/Soundness/Realizability.v +++ b/theories/Core/Soundness/Realizability.v @@ -1,9 +1,9 @@ From Coq Require Import Nat. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Import Realizability. -From Mcltt.Core.Soundness.LogicalRelation Require Export Core. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Soundness.LogicalRelation Require Export Core. Import Domain_Notations. Open Scope list_scope. @@ -95,7 +95,7 @@ Proof. Qed. #[local] -Hint Rewrite -> wf_sub_eq_extend_compose using mauto 4 : mcltt. +Hint Rewrite -> wf_sub_eq_extend_compose using mauto 4 : mctt. Theorem realize_glu_univ_elem_gen : forall a i P El, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> @@ -197,7 +197,7 @@ Proof. simplify_evals. destruct (H2 _ ltac:(eassumption) _ ltac:(eassumption)) as [? []]. assert (IEl {{{ Δ, IT[σ] }}} {{{ IT[σ][Wk] }}} {{{ #0 }}} d{{{ ⇑! a (length Δ) }}}) by mauto 3 using var_glu_elem_bot. - autorewrite with mcltt in H31. + autorewrite with mctt in H31. specialize (H14 {{{ Δ, IT[σ] }}} {{{ σ∘Wk }}} _ _ ltac:(mauto) ltac:(eassumption) ltac:(eassumption)). specialize (H8 _ _ _ ltac:(eassumption) ltac:(eassumption)) as []. etransitivity; [| eapply H33]; mauto 3. @@ -219,7 +219,7 @@ Proof. unshelve (econstructor; eauto). + trivial. + eassert {{ Δ ⊢ M[σ] N : ^_ }} by (eapply wf_app'; eassumption). - autorewrite with mcltt in H25. + autorewrite with mctt in H25. trivial. + mauto using domain_app_per. + intros. @@ -227,7 +227,7 @@ Proof. progressive_invert H26. destruct (H15 _ _ _ _ _ ltac:(eassumption) ltac:(eassumption) ltac:(eassumption) equiv_n). handle_functional_glu_univ_elem. - autorewrite with mcltt. + autorewrite with mctt. etransitivity. * rewrite sub_decompose_q_typ; mauto 4. @@ -240,7 +240,7 @@ Proof. bulky_rewrite_in H12. -- rewrite <- @exp_eq_sub_compose_typ; mauto 3. -- econstructor; mauto 3. - autorewrite with mcltt. + autorewrite with mctt. rewrite <- @exp_eq_sub_compose_typ; mauto 3. - handle_functional_glu_univ_elem. @@ -263,9 +263,9 @@ Proof. destruct (H11 _ _ _ ltac:(eassumption) ltac:(eassumption)) as []. specialize (H29 _ _ _ H19 H9). rewrite H5 in *. - autorewrite with mcltt. + autorewrite with mctt. eassert {{ Δ ⊢ M[σ] : ^_ }} by (mauto 2). - autorewrite with mcltt in H30. + autorewrite with mctt in H30. rewrite @wf_exp_eq_pi_eta' with (M := {{{ M[σ] }}}); [| trivial]. cbn [nf_to_exp]. eapply wf_exp_eq_fn_cong'; eauto. @@ -275,7 +275,7 @@ Proof. simplify_evals. destruct (H2 _ ltac:(eassumption) _ ltac:(eassumption)) as [? []]. specialize (H12 _ _ _ _ ltac:(trivial) (var_glu_elem_bot _ _ _ _ _ _ H H10)). - autorewrite with mcltt in H12. + autorewrite with mctt in H12. specialize (H14 {{{Δ, IT[σ]}}} {{{σ ∘ Wk}}} _ _ ltac:(mauto) ltac:(eassumption) ltac:(eassumption)) as [? []]. apply_equiv_left. destruct_rel_mod_app. @@ -351,7 +351,7 @@ Proof. Qed. #[export] -Hint Resolve realize_glu_typ_top realize_glu_elem_top : mcltt. +Hint Resolve realize_glu_typ_top realize_glu_elem_top : mctt. Corollary var0_glu_elem : forall {i a P El Γ A}, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> diff --git a/theories/Core/Soundness/SubstitutionCases.v b/theories/Core/Soundness/SubstitutionCases.v index a922327..3252f9e 100644 --- a/theories/Core/Soundness/SubstitutionCases.v +++ b/theories/Core/Soundness/SubstitutionCases.v @@ -1,8 +1,8 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import FundamentalTheorem. -From Mcltt.Core.Semantic Require Import Realizability. -From Mcltt.Core.Soundness Require Import LogicalRelation SubtypingCases TermStructureCases UniverseCases. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import FundamentalTheorem. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Soundness Require Import LogicalRelation SubtypingCases TermStructureCases UniverseCases. Import Domain_Notations. Lemma presup_glu_rel_sub : forall {Γ σ Δ}, @@ -23,7 +23,7 @@ Proof. Qed. #[export] -Hint Resolve presup_left_glu_rel_sub : mcltt. +Hint Resolve presup_left_glu_rel_sub : mctt. Lemma presup_right_glu_rel_sub : forall {Γ σ Δ}, {{ Γ ⊩s σ : Δ }} -> @@ -34,7 +34,7 @@ Proof. Qed. #[export] -Hint Resolve presup_right_glu_rel_sub : mcltt. +Hint Resolve presup_right_glu_rel_sub : mctt. Lemma glu_rel_sub_id : forall {Γ}, {{ ⊩ Γ }} -> @@ -48,7 +48,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_sub_id : mcltt. +Hint Resolve glu_rel_sub_id : mctt. Lemma glu_rel_sub_weaken : forall {Γ A}, {{ ⊩ Γ, A }} -> @@ -64,7 +64,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_sub_weaken : mcltt. +Hint Resolve glu_rel_sub_weaken : mctt. Lemma glu_rel_sub_compose : forall {Γ1 σ2 Γ2 σ1 Γ3}, {{ Γ1 ⊩s σ2 : Γ2 }} -> @@ -88,7 +88,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_sub_compose : mcltt. +Hint Resolve glu_rel_sub_compose : mctt. Lemma glu_rel_sub_extend : forall {Γ σ Δ M A i}, {{ Γ ⊩s σ : Δ }} -> @@ -145,4 +145,4 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_sub_extend : mcltt. +Hint Resolve glu_rel_sub_extend : mctt. diff --git a/theories/Core/Soundness/SubtypingCases.v b/theories/Core/Soundness/SubtypingCases.v index ecd5af8..3f88be3 100644 --- a/theories/Core/Soundness/SubtypingCases.v +++ b/theories/Core/Soundness/SubtypingCases.v @@ -1,8 +1,8 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import FundamentalTheorem. -From Mcltt.Core.Semantic Require Import Realizability. -From Mcltt.Core.Soundness Require Import LogicalRelation. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import FundamentalTheorem. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Soundness Require Import LogicalRelation. Import Domain_Notations. Lemma glu_rel_exp_subtyp : forall {Γ M A A' i}, @@ -34,7 +34,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_subtyp : mcltt. +Hint Resolve glu_rel_exp_subtyp : mctt. Lemma glu_rel_sub_subtyp : forall {Γ σ Δ Δ'}, {{ Γ ⊩s σ : Δ }} -> @@ -52,7 +52,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_sub_subtyp : mcltt. +Hint Resolve glu_rel_sub_subtyp : mctt. Lemma glu_rel_exp_conv : forall {Γ M A A' i}, {{ Γ ⊩ M : A }} -> @@ -64,7 +64,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_conv : mcltt. +Hint Resolve glu_rel_exp_conv : mctt. Lemma glu_rel_sub_conv : forall {Γ σ Δ Δ'}, {{ Γ ⊩s σ : Δ }} -> @@ -76,4 +76,4 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_sub_conv : mcltt. +Hint Resolve glu_rel_sub_conv : mctt. diff --git a/theories/Core/Soundness/TermStructureCases.v b/theories/Core/Soundness/TermStructureCases.v index 5f359de..b625891 100644 --- a/theories/Core/Soundness/TermStructureCases.v +++ b/theories/Core/Soundness/TermStructureCases.v @@ -1,8 +1,8 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import FundamentalTheorem. -From Mcltt.Core.Semantic Require Import Realizability. -From Mcltt.Core.Soundness Require Import LogicalRelation. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import FundamentalTheorem. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Soundness Require Import LogicalRelation. Import Domain_Notations. Lemma presup_glu_rel_exp : forall {Γ M A}, @@ -24,7 +24,7 @@ Proof. Qed. #[export] -Hint Resolve presup_ctx_glu_rel_exp : mcltt. +Hint Resolve presup_ctx_glu_rel_exp : mctt. Lemma presup_typ_glu_rel_exp : forall {Γ M A}, {{ Γ ⊩ M : A }} -> @@ -35,7 +35,7 @@ Proof. Qed. #[export] -Hint Resolve presup_typ_glu_rel_exp : mcltt. +Hint Resolve presup_typ_glu_rel_exp : mctt. Lemma glu_rel_exp_vlookup : forall {Γ x A}, {{ ⊩ Γ }} -> @@ -78,7 +78,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_vlookup : mcltt. +Hint Resolve glu_rel_exp_vlookup : mctt. Lemma glu_rel_exp_sub : forall {Γ σ Δ M A}, {{ Γ ⊩s σ : Δ }} -> @@ -106,4 +106,4 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_sub : mcltt. +Hint Resolve glu_rel_exp_sub : mctt. diff --git a/theories/Core/Soundness/UniverseCases.v b/theories/Core/Soundness/UniverseCases.v index ec94182..b9aa78d 100644 --- a/theories/Core/Soundness/UniverseCases.v +++ b/theories/Core/Soundness/UniverseCases.v @@ -1,8 +1,8 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Completeness Require Import FundamentalTheorem. -From Mcltt.Core.Semantic Require Import Realizability. -From Mcltt.Core.Soundness Require Import LogicalRelation SubtypingCases TermStructureCases. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Completeness Require Import FundamentalTheorem. +From Mctt.Core.Semantic Require Import Realizability. +From Mctt.Core.Soundness Require Import LogicalRelation SubtypingCases TermStructureCases. Import Domain_Notations. Lemma glu_rel_exp_of_typ : forall {Γ Sb A i}, @@ -41,7 +41,7 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_typ : mcltt. +Hint Resolve glu_rel_exp_typ : mctt. Lemma glu_rel_exp_clean_inversion2' : forall {i Γ Sb M}, {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> @@ -75,4 +75,4 @@ Proof. Qed. #[export] -Hint Resolve glu_rel_exp_sub_typ : mcltt. +Hint Resolve glu_rel_exp_sub_typ : mctt. diff --git a/theories/Core/Soundness/Weakening/Definitions.v b/theories/Core/Soundness/Weakening/Definitions.v index b273e9a..c10d428 100644 --- a/theories/Core/Soundness/Weakening/Definitions.v +++ b/theories/Core/Soundness/Weakening/Definitions.v @@ -1,5 +1,5 @@ -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic Require Export SystemOpt. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic Require Export SystemOpt. Import Syntax_Notations. Generalizable All Variables. @@ -18,4 +18,4 @@ Inductive weakening : ctx -> sub -> ctx -> Prop := where "Γ ⊢w σ : Δ" := (weakening Γ σ Δ) (in custom judg) : type_scope. #[export] - Hint Constructors weakening : mcltt. + Hint Constructors weakening : mctt. diff --git a/theories/Core/Soundness/Weakening/Lemmas.v b/theories/Core/Soundness/Weakening/Lemmas.v index e4cd71a..5850712 100644 --- a/theories/Core/Soundness/Weakening/Lemmas.v +++ b/theories/Core/Soundness/Weakening/Lemmas.v @@ -1,9 +1,9 @@ From Coq Require Import Program.Equality. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Soundness.Weakening Require Import Definitions. -From Mcltt.Core.Syntactic Require Export Corollaries. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Soundness.Weakening Require Import Definitions. +From Mctt.Core.Syntactic Require Export Corollaries. Import Syntax_Notations. Lemma weakening_escape : forall Γ σ Δ, @@ -18,7 +18,7 @@ Proof. Qed. #[export] -Hint Resolve weakening_escape : mcltt. +Hint Resolve weakening_escape : mctt. Ltac saturate_weakening_escape1 := @@ -67,7 +67,7 @@ Proof. Qed. #[export] -Hint Resolve ctxsub_weakening weakening_conv : mcltt. +Hint Resolve ctxsub_weakening weakening_conv : mctt. Lemma weakening_compose : forall Γ' σ' Γ'', {{ Γ' ⊢w σ' : Γ'' }} -> @@ -86,7 +86,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve weakening_compose : mcltt. +Hint Resolve weakening_compose : mctt. Lemma weakening_id : forall Γ, {{ ⊢ Γ }} -> @@ -104,4 +104,4 @@ Proof. Qed. #[export] -Hint Resolve weakening_id weakening_wk : mcltt. +Hint Resolve weakening_id weakening_wk : mctt. diff --git a/theories/Core/Syntactic/CoreInversions.v b/theories/Core/Syntactic/CoreInversions.v index 19da398..4bbda57 100644 --- a/theories/Core/Syntactic/CoreInversions.v +++ b/theories/Core/Syntactic/CoreInversions.v @@ -1,7 +1,7 @@ From Coq Require Import Setoid. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic Require Export CtxEq. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic Require Export CtxEq. Import Syntax_Notations. Lemma wf_typ_inversion : forall {Γ i A}, @@ -13,7 +13,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve wf_typ_inversion : mcltt. +Hint Resolve wf_typ_inversion : mctt. Lemma wf_nat_inversion : forall Γ A, {{ Γ ⊢ ℕ : A }} -> @@ -25,7 +25,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve wf_nat_inversion : mcltt. +Hint Resolve wf_nat_inversion : mctt. Corollary wf_zero_inversion : forall Γ A, {{ Γ ⊢ zero : A }} -> @@ -37,7 +37,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve wf_zero_inversion : mcltt. +Hint Resolve wf_zero_inversion : mctt. Corollary wf_succ_inversion : forall Γ A M, {{ Γ ⊢ succ M : A }} -> @@ -50,7 +50,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve wf_succ_inversion : mcltt. +Hint Resolve wf_succ_inversion : mctt. Lemma wf_natrec_inversion : forall Γ A M A' MZ MS, {{ Γ ⊢ rec M return A' | zero -> MZ | succ -> MS end : A }} -> @@ -64,7 +64,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve wf_natrec_inversion : mcltt. +Hint Resolve wf_natrec_inversion : mctt. Lemma wf_pi_inversion : forall {Γ A B C}, {{ Γ ⊢ Π A B : C }} -> @@ -77,7 +77,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve wf_pi_inversion : mcltt. +Hint Resolve wf_pi_inversion : mctt. Corollary wf_pi_inversion' : forall {Γ A B i}, {{ Γ ⊢ Π A B : Type@i }} -> @@ -92,7 +92,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve wf_pi_inversion' : mcltt. +Hint Resolve wf_pi_inversion' : mctt. Corollary wf_fn_inversion : forall {Γ A M C}, {{ Γ ⊢ λ A M : C }} -> @@ -106,7 +106,7 @@ Proof with solve [mauto using lift_exp_max_left, lift_exp_max_right]. Qed. #[export] -Hint Resolve wf_fn_inversion : mcltt. +Hint Resolve wf_fn_inversion : mctt. Lemma wf_app_inversion : forall {Γ M N C}, {{ Γ ⊢ M N : C }} -> @@ -120,7 +120,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve wf_app_inversion : mcltt. +Hint Resolve wf_app_inversion : mctt. Lemma wf_vlookup_inversion : forall {Γ x A}, {{ Γ ⊢ #x : A }} -> @@ -133,7 +133,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve wf_vlookup_inversion : mcltt. +Hint Resolve wf_vlookup_inversion : mctt. Lemma wf_exp_sub_inversion : forall {Γ M σ A}, {{ Γ ⊢ M[σ] : A }} -> @@ -148,7 +148,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve wf_exp_sub_inversion : mcltt. +Hint Resolve wf_exp_sub_inversion : mctt. (** We omit [wf_conv] and [wf_cumu] as they do not give useful inversions *) @@ -161,7 +161,7 @@ Proof. Qed. #[export] -Hint Resolve wf_sub_id_inversion : mcltt. +Hint Resolve wf_sub_id_inversion : mctt. Lemma wf_sub_weaken_inversion : forall {Γ Δ}, {{ Γ ⊢s Wk : Δ }} -> @@ -175,7 +175,7 @@ Proof. Qed. #[export] -Hint Resolve wf_sub_weaken_inversion : mcltt. +Hint Resolve wf_sub_weaken_inversion : mctt. Lemma wf_sub_compose_inversion : forall {Γ1 σ1 σ2 Γ3}, {{ Γ1 ⊢s σ1 ∘ σ2 : Γ3 }} -> @@ -190,7 +190,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve wf_sub_compose_inversion : mcltt. +Hint Resolve wf_sub_compose_inversion : mctt. Lemma wf_sub_extend_inversion : forall {Γ σ M Δ}, {{ Γ ⊢s σ,,M : Δ }} -> @@ -204,4 +204,4 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve wf_sub_extend_inversion : mcltt. +Hint Resolve wf_sub_extend_inversion : mctt. diff --git a/theories/Core/Syntactic/Corollaries.v b/theories/Core/Syntactic/Corollaries.v index 111da3a..f3d5b87 100644 --- a/theories/Core/Syntactic/Corollaries.v +++ b/theories/Core/Syntactic/Corollaries.v @@ -1,7 +1,7 @@ From Coq Require Import Setoid Nat. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic Require Export SystemOpt. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic Require Export SystemOpt. Import Syntax_Notations. Corollary sub_id_typ : forall Γ M A, @@ -14,7 +14,7 @@ Proof. Qed. #[export] -Hint Resolve sub_id_typ : mcltt. +Hint Resolve sub_id_typ : mctt. Corollary invert_sub_id : forall Γ M A, {{ Γ ⊢ M[Id] : A }} -> @@ -25,7 +25,7 @@ Proof. Qed. #[export] -Hint Resolve invert_sub_id : mcltt. +Hint Resolve invert_sub_id : mctt. Corollary invert_sub_id_typ : forall Γ M A, {{ Γ ⊢ M : A[Id] }} -> @@ -34,11 +34,11 @@ Proof. intros. gen_presups. assert {{ Γ ⊢ A : Type@i }} by mauto. - autorewrite with mcltt in *; eassumption. + autorewrite with mctt in *; eassumption. Qed. #[export] -Hint Resolve invert_sub_id_typ : mcltt. +Hint Resolve invert_sub_id_typ : mctt. Lemma invert_compose_id : forall {Γ σ Δ}, {{ Γ ⊢s σ∘Id : Δ }} -> @@ -49,7 +49,7 @@ Proof. Qed. #[export] -Hint Resolve invert_compose_id : mcltt. +Hint Resolve invert_compose_id : mctt. Add Parametric Morphism i Γ Δ : a_sub with signature wf_exp_eq Δ {{{ Type@i }}} ==> wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong. @@ -106,7 +106,7 @@ Proof. - rewrite <- @exp_eq_sub_compose_typ; mauto 4. Qed. #[export] - Hint Resolve sub_q_eq : mcltt. + Hint Resolve sub_q_eq : mctt. Lemma wf_subtyp_subst_eq : forall Δ A B, {{ Δ ⊢ A ⊆ B }} -> @@ -118,9 +118,9 @@ Proof. - eapply wf_subtyp_refl'. eapply wf_exp_eq_conv; mauto 4. - etransitivity; mauto 4. - - autorewrite with mcltt. + - autorewrite with mctt. mauto 2. - - autorewrite with mcltt. + - autorewrite with mctt. eapply wf_subtyp_pi'; mauto. Qed. @@ -133,7 +133,7 @@ Proof. intros; mauto 2 using wf_subtyp_subst_eq. Qed. #[export] -Hint Resolve wf_subtyp_subst_eq wf_subtyp_subst : mcltt. +Hint Resolve wf_subtyp_subst_eq wf_subtyp_subst : mctt. Lemma exp_typ_sub_lhs : forall {Γ σ Δ i}, {{ Γ ⊢s σ : Δ }} -> @@ -142,7 +142,7 @@ Proof. intros; mauto 4. Qed. #[export] -Hint Resolve exp_typ_sub_lhs : mcltt. +Hint Resolve exp_typ_sub_lhs : mctt. Lemma exp_nat_sub_lhs : forall {Γ σ Δ i}, {{ Γ ⊢s σ : Δ }} -> @@ -151,7 +151,7 @@ Proof. intros; mauto 4. Qed. #[export] -Hint Resolve exp_nat_sub_lhs : mcltt. +Hint Resolve exp_nat_sub_lhs : mctt. Lemma exp_zero_sub_lhs : forall {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> @@ -160,7 +160,7 @@ Proof. intros; mauto 4. Qed. #[export] -Hint Resolve exp_zero_sub_lhs : mcltt. +Hint Resolve exp_zero_sub_lhs : mctt. Lemma exp_succ_sub_lhs : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> @@ -170,7 +170,7 @@ Proof. intros; mauto 3. Qed. #[export] -Hint Resolve exp_succ_sub_lhs : mcltt. +Hint Resolve exp_succ_sub_lhs : mctt. Lemma exp_succ_sub_rhs : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> @@ -180,7 +180,7 @@ Proof. intros; mauto 3. Qed. #[export] -Hint Resolve exp_succ_sub_rhs : mcltt. +Hint Resolve exp_succ_sub_rhs : mctt. Lemma sub_decompose_q : forall Γ S i σ Δ Δ' τ t, {{ Γ ⊢ S : Type@i }} -> @@ -190,7 +190,7 @@ Lemma sub_decompose_q : forall Γ S i σ Δ Δ' τ t, {{ Δ' ⊢s q σ ∘ (τ ,, t) ≈ σ ∘ τ ,, t : Γ, S }}. Proof. intros. gen_presups. - simpl. autorewrite with mcltt. + simpl. autorewrite with mctt. symmetry. rewrite wf_sub_eq_extend_compose; mauto 3; [| mauto @@ -202,7 +202,7 @@ Proof. Qed. #[local] -Hint Rewrite -> @sub_decompose_q using mauto 4 : mcltt. +Hint Rewrite -> @sub_decompose_q using mauto 4 : mctt. Lemma sub_decompose_q_typ : forall Γ S T i σ Δ Δ' τ t, {{ Γ, S ⊢ T : Type@i }} -> @@ -212,7 +212,7 @@ Lemma sub_decompose_q_typ : forall Γ S T i σ Δ Δ' τ t, {{ Δ' ⊢ T[σ∘τ,,t] ≈ T[q σ][τ,,t] : Type@i}}. Proof. intros. gen_presups. - autorewrite with mcltt. + autorewrite with mctt. eapply exp_eq_sub_cong_typ2'; [mauto 2 | econstructor; mauto 4 |]. eapply sub_eq_refl; econstructor; mauto 3. Qed. @@ -228,17 +228,17 @@ Proof. assert {{ ⊢ Γ, A }} by mauto 3. assert {{ Δ, A[σ] ⊢s q σ : Γ, A }} by mauto 2. assert {{ Δ' ⊢s τ,,M : Δ, A[σ] }} by mauto 3. - transitivity {{{ Wk∘((σ∘τ),,M) }}}; [| autorewrite with mcltt; mauto 3]. + transitivity {{{ Wk∘((σ∘τ),,M) }}}; [| autorewrite with mctt; mauto 3]. eapply wf_sub_eq_compose_cong; [| mauto 2]. - autorewrite with mcltt; econstructor; mauto 3. + autorewrite with mctt; econstructor; mauto 3. assert {{ Δ' ⊢ A[σ∘τ] ≈ A[σ][τ] : Type@i }} as -> by mauto 3. mauto 3. Qed. #[export] -Hint Resolve sub_eq_p_q_sigma_compose_tau_extend : mcltt. +Hint Resolve sub_eq_p_q_sigma_compose_tau_extend : mctt. #[export] -Hint Rewrite -> @sub_eq_p_q_sigma_compose_tau_extend using mauto 4 : mcltt. +Hint Rewrite -> @sub_eq_p_q_sigma_compose_tau_extend using mauto 4 : mctt. Lemma exp_eq_natrec_cong_rhs_typ : forall {Γ M M' A A' i}, {{ Γ, ℕ ⊢ A ≈ A' : Type@i }} -> @@ -253,7 +253,7 @@ Proof. mauto 3. Qed. #[export] -Hint Resolve exp_eq_natrec_cong_rhs_typ : mcltt. +Hint Resolve exp_eq_natrec_cong_rhs_typ : mctt. (** This works for both natrec_sub and app_sub cases *) Lemma exp_eq_elim_sub_lhs_typ_gen : forall {Γ σ Δ M A B i}, @@ -266,13 +266,13 @@ Proof. assert {{ ⊢ Δ }} by mauto 2. assert (exists j, {{ Δ ⊢ A : Type@j }}) as [] by mauto 3. assert {{ Δ ⊢s Id,,M : Δ, A }} by mauto 3. - autorewrite with mcltt. + autorewrite with mctt. assert {{ Γ ⊢ M[σ] : A[σ] }} by mauto 2. assert {{ Γ ⊢s σ,,M[σ] ≈ (Id,,M)∘σ : Δ, A }} as -> by mauto 3. mauto 4. Qed. #[export] -Hint Resolve exp_eq_elim_sub_lhs_typ_gen : mcltt. +Hint Resolve exp_eq_elim_sub_lhs_typ_gen : mctt. (** This works for both natrec_sub and app_sub cases *) Lemma exp_eq_elim_sub_rhs_typ : forall {Γ σ Δ M A B i}, @@ -283,12 +283,12 @@ Lemma exp_eq_elim_sub_rhs_typ : forall {Γ σ Δ M A B i}, Proof. intros. assert (exists j, {{ Δ ⊢ A : Type@j }}) as [] by mauto 3. - autorewrite with mcltt. + autorewrite with mctt. assert {{ Γ ⊢s σ∘Id ≈ σ : Δ }} by mauto 3. assert {{ Γ ⊢s σ,,M ≈ (σ∘Id),,M : Δ, A }} as <-; mauto 4. Qed. #[export] -Hint Resolve exp_eq_elim_sub_rhs_typ : mcltt. +Hint Resolve exp_eq_elim_sub_rhs_typ : mctt. Lemma exp_eq_sub_cong_typ2 : forall {Δ Γ A σ τ i}, {{ Δ ⊢ A : Type@i }} -> @@ -300,9 +300,9 @@ Proof with mautosolve 3. mauto 3. Qed. #[export] -Hint Resolve exp_eq_sub_cong_typ2 : mcltt. +Hint Resolve exp_eq_sub_cong_typ2 : mctt. #[export] -Remove Hints exp_eq_sub_cong_typ2' : mcltt. +Remove Hints exp_eq_sub_cong_typ2' : mctt. Lemma exp_eq_nat_beta_succ_rhs_typ_gen : forall {Γ σ Δ i A M N}, {{ Γ ⊢s σ : Δ }} -> @@ -320,10 +320,10 @@ Proof. assert {{ Γ ⊢s σ,,M : Δ, ℕ }} by mauto 4. assert {{ Γ ⊢s σ,,M,,N : Δ, ℕ, A }} by mauto 3. assert {{ Γ ⊢s σ,,M,,N : Δ, ℕ, A }} by mauto 3. - autorewrite with mcltt. + autorewrite with mctt. assert {{ Γ ⊢s (Wk∘Wk,,succ #1)∘(σ,,M,,N) ≈ ((Wk∘Wk)∘(σ,,M,,N)),,(succ #1)[σ,,M,,N] : Δ, ℕ }} as -> by mauto 4. assert {{ Γ ⊢s (Wk∘Wk)∘(σ,,M,,N) ≈ Wk∘(Wk∘(σ,,M,,N)) : Δ }} by mauto 3. - assert {{ Γ ⊢s Wk∘(σ,,M,,N) ≈ σ,,M : Δ, ℕ }} by (autorewrite with mcltt; mauto 3). + assert {{ Γ ⊢s Wk∘(σ,,M,,N) ≈ σ,,M : Δ, ℕ }} by (autorewrite with mctt; mauto 3). assert {{ Γ ⊢s (Wk∘Wk)∘(σ,,M,,N) ≈ Wk∘(σ,,M) : Δ }} by (unshelve bulky_rewrite; constructor). assert {{ Γ ⊢s (Wk∘Wk)∘(σ,,M,,N) ≈ σ : Δ }} by bulky_rewrite. assert {{ Γ ⊢ (succ #1)[σ,,M,,N] ≈ succ (#1[σ,,M,,N]) : ℕ }} by mauto 3. @@ -333,7 +333,7 @@ Proof. mauto 3. Qed. #[export] -Hint Resolve exp_eq_nat_beta_succ_rhs_typ_gen : mcltt. +Hint Resolve exp_eq_nat_beta_succ_rhs_typ_gen : mctt. Lemma exp_pi_sub_lhs : forall {Γ σ Δ A B i}, {{ Γ ⊢s σ : Δ }} -> @@ -345,7 +345,7 @@ Proof. mauto 4. Qed. #[export] -Hint Resolve exp_pi_sub_lhs : mcltt. +Hint Resolve exp_pi_sub_lhs : mctt. Lemma exp_pi_sub_rhs : forall {Γ σ Δ A B i}, {{ Γ ⊢s σ : Δ }} -> @@ -357,7 +357,7 @@ Proof. econstructor; mauto 3. Qed. #[export] -Hint Resolve exp_pi_sub_rhs : mcltt. +Hint Resolve exp_pi_sub_rhs : mctt. Lemma exp_pi_eta_rhs_body : forall {Γ A B M}, {{ Γ ⊢ M : Π A B }} -> @@ -369,23 +369,23 @@ Proof. assert {{ Γ, A ⊢s Wk : Γ }} by mauto 3. assert {{ Γ, A, A[Wk] ⊢s q Wk : Γ, A }} by mauto 3. assert {{ Γ, A ⊢ M[Wk] : (Π A B)[Wk] }} by mauto 3. - assert {{ Γ, A ⊢ Π A[Wk] B[q Wk] ≈ (Π A B)[Wk] : Type@i }} by (autorewrite with mcltt; mauto 3). + assert {{ Γ, A ⊢ Π A[Wk] B[q Wk] ≈ (Π A B)[Wk] : Type@i }} by (autorewrite with mctt; mauto 3). assert {{ Γ, A ⊢ M[Wk] : Π A[Wk] B[q Wk] }} by mauto 3. econstructor; [econstructor; revgoals; mauto 3 | mauto 3 |]. eapply wf_subtyp_refl'. - autorewrite with mcltt. + autorewrite with mctt. - transitivity {{{ B[Id] }}}; [| mauto 3]. eapply exp_eq_sub_cong_typ2; mauto 4. transitivity {{{ Wk,,#0 }}}; [| mauto 3]. econstructor; mauto 3. - autorewrite with mcltt. + autorewrite with mctt. mauto 3. - econstructor; mauto 3. - autorewrite with mcltt. + autorewrite with mctt. mauto 3. Qed. #[export] -Hint Resolve exp_pi_eta_rhs_body : mcltt. +Hint Resolve exp_pi_eta_rhs_body : mctt. (** This works for both var_0 and var_S cases *) Lemma exp_eq_var_sub_rhs_typ_gen : forall {Γ σ Δ i A M}, @@ -396,11 +396,11 @@ Lemma exp_eq_var_sub_rhs_typ_gen : forall {Γ σ Δ i A M}, Proof. intros. assert {{ Γ ⊢s σ,,M : Δ, A }} by mauto 3. - autorewrite with mcltt. + autorewrite with mctt. mauto 3. Qed. #[export] -Hint Resolve exp_eq_var_sub_rhs_typ_gen : mcltt. +Hint Resolve exp_eq_var_sub_rhs_typ_gen : mctt. Lemma exp_sub_decompose_double_q_with_id_double_extend : forall Γ A B C σ Δ M N L, {{ Γ, B, C ⊢ M : A }} -> @@ -429,7 +429,7 @@ Proof. Qed. #[export] -Hint Resolve exp_sub_decompose_double_q_with_id_double_extend : mcltt. +Hint Resolve exp_sub_decompose_double_q_with_id_double_extend : mctt. Lemma sub_eq_q_compose : forall {Γ A i σ Δ τ Δ'}, {{ Γ ⊢ A : Type@i }} -> @@ -465,9 +465,9 @@ Proof. Qed. #[export] -Hint Resolve sub_eq_q_compose : mcltt. +Hint Resolve sub_eq_q_compose : mctt. #[export] -Hint Rewrite -> @sub_eq_q_compose using mauto 4 : mcltt. +Hint Rewrite -> @sub_eq_q_compose using mauto 4 : mctt. Lemma sub_eq_q_compose_nat : forall {Γ σ Δ τ Δ'}, {{ Δ ⊢s σ : Γ }} -> @@ -483,9 +483,9 @@ Proof. Qed. #[export] -Hint Resolve sub_eq_q_compose_nat : mcltt. +Hint Resolve sub_eq_q_compose_nat : mctt. #[export] -Hint Rewrite -> @sub_eq_q_compose_nat using mauto 4 : mcltt. +Hint Rewrite -> @sub_eq_q_compose_nat using mauto 4 : mctt. Lemma exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 : forall {Δ σ Γ i A}, {{ Δ ⊢s σ : Γ }} -> @@ -505,4 +505,4 @@ Proof. Qed. #[export] -Hint Resolve exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 : mcltt. +Hint Resolve exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1 : mctt. diff --git a/theories/Core/Syntactic/CtxEq.v b/theories/Core/Syntactic/CtxEq.v index 85894d2..01f881e 100644 --- a/theories/Core/Syntactic/CtxEq.v +++ b/theories/Core/Syntactic/CtxEq.v @@ -1,6 +1,6 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic Require Export CtxSub. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic Require Export CtxSub. Import Syntax_Notations. Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}. @@ -9,7 +9,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve ctx_eq_refl : mcltt. +Hint Resolve ctx_eq_refl : mctt. Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}. Proof. @@ -19,7 +19,7 @@ Proof. Qed. #[export] -Hint Resolve ctx_eq_sym : mcltt. +Hint Resolve ctx_eq_sym : mctt. Lemma ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}. Proof. mauto. Qed. @@ -37,7 +37,7 @@ Lemma ctxeq_subtyp : forall {Γ Δ A B}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ A ⊆ Proof. mauto. Qed. #[export] -Hint Resolve ctxeq_exp ctxeq_exp_eq ctxeq_sub ctxeq_sub_eq ctxeq_subtyp : mcltt. +Hint Resolve ctxeq_exp ctxeq_exp_eq ctxeq_sub ctxeq_sub_eq ctxeq_subtyp : mctt. Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 ≈ Γ2 }} -> {{ ⊢ Γ0 ≈ Γ2 }}. @@ -58,7 +58,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve ctx_eq_trans : mcltt. +Hint Resolve ctx_eq_trans : mctt. #[export] Instance wf_ctx_PER : PER wf_ctx_eq. diff --git a/theories/Core/Syntactic/CtxSub.v b/theories/Core/Syntactic/CtxSub.v index a042352..d641a6c 100644 --- a/theories/Core/Syntactic/CtxSub.v +++ b/theories/Core/Syntactic/CtxSub.v @@ -1,6 +1,6 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic Require Export System. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic Require Export System. Import Syntax_Notations. Lemma ctx_sub_refl : forall {Γ}, @@ -11,7 +11,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve ctx_sub_refl : mcltt. +Hint Resolve ctx_sub_refl : mctt. Module ctxsub_judg. #[local] @@ -107,7 +107,7 @@ Module ctxsub_judg. Qed. #[export] - Hint Resolve ctxsub_exp ctxsub_exp_eq ctxsub_sub ctxsub_sub_eq ctxsub_subtyp : mcltt. + Hint Resolve ctxsub_exp ctxsub_exp_eq ctxsub_sub ctxsub_sub_eq ctxsub_subtyp : mctt. End ctxsub_judg. Export ctxsub_judg. @@ -124,7 +124,7 @@ Proof. Qed. #[export] - Hint Resolve wf_ctx_sub_trans : mcltt. + Hint Resolve wf_ctx_sub_trans : mctt. #[export] Instance wf_ctx_sub_trans_ins : Transitive wf_ctx_sub. diff --git a/theories/Core/Syntactic/Presup.v b/theories/Core/Syntactic/Presup.v index 36916fb..d2c8d5e 100644 --- a/theories/Core/Syntactic/Presup.v +++ b/theories/Core/Syntactic/Presup.v @@ -1,6 +1,6 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic Require Export CtxEq. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic Require Export CtxEq. Import Syntax_Notations. Lemma presup_exp_eq_natrec_cong_right : forall {Γ i A A' MZ' MS' M M'}, @@ -33,7 +33,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_natrec_cong_right : mcltt. +Hint Resolve presup_exp_eq_natrec_cong_right : mctt. Lemma presup_exp_eq_natrec_sub_left : forall {Γ σ Δ i A MZ MS M}, {{ ⊢ Γ }} -> @@ -58,7 +58,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_natrec_sub_left : mcltt. +Hint Resolve presup_exp_eq_natrec_sub_left : mctt. Lemma presup_exp_eq_natrec_sub_right : forall {Γ σ Δ i A MZ MS M}, {{ ⊢ Γ }} -> @@ -112,7 +112,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_natrec_sub_right : mcltt. +Hint Resolve presup_exp_eq_natrec_sub_right : mctt. Lemma presup_exp_eq_beta_succ_right : forall {Γ i A MZ MS M}, {{ ⊢ Γ, ℕ }} -> @@ -156,7 +156,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_beta_succ_right : mcltt. +Hint Resolve presup_exp_eq_beta_succ_right : mctt. Lemma presup_exp_eq_fn_cong_right : forall {Γ i A A' j B M'}, {{ ⊢ Γ }} -> @@ -179,7 +179,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_fn_cong_right : mcltt. +Hint Resolve presup_exp_eq_fn_cong_right : mctt. Lemma presup_exp_eq_fn_sub_right : forall {Γ σ Δ i A j B M}, {{ ⊢ Γ }} -> @@ -204,7 +204,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_fn_sub_right : mcltt. +Hint Resolve presup_exp_eq_fn_sub_right : mctt. Lemma presup_exp_eq_app_cong_right : forall {Γ i A B M' N N'}, {{ ⊢ Γ }} -> @@ -227,7 +227,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_app_cong_right : mcltt. +Hint Resolve presup_exp_eq_app_cong_right : mctt. Lemma presup_exp_eq_app_sub_left : forall {Γ σ Δ i A B M N}, {{ ⊢ Γ }} -> @@ -258,7 +258,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_app_sub_left : mcltt. +Hint Resolve presup_exp_eq_app_sub_left : mctt. Lemma presup_exp_eq_app_sub_right : forall {Γ σ Δ i A B M N}, {{ ⊢ Γ }} -> @@ -287,7 +287,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_app_sub_right : mcltt. +Hint Resolve presup_exp_eq_app_sub_right : mctt. Lemma presup_exp_eq_pi_eta_right : forall {Γ i A B M}, {{ ⊢ Γ }} -> @@ -312,7 +312,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_pi_eta_right : mcltt. +Hint Resolve presup_exp_eq_pi_eta_right : mctt. Lemma presup_exp_eq_prop_eq_var0 : forall {Γ i A}, {{ Γ ⊢ A : Type@i }} -> @@ -326,7 +326,7 @@ Proof. Qed. #[export] -Hint Resolve presup_exp_eq_prop_eq_var0 : mcltt. +Hint Resolve presup_exp_eq_prop_eq_var0 : mctt. Lemma presup_exp_eq_prop_eq_var1 : forall {Γ i A}, {{ Γ ⊢ A : Type@i }} -> @@ -340,7 +340,7 @@ Proof. Qed. #[export] -Hint Resolve presup_exp_eq_prop_eq_var1 : mcltt. +Hint Resolve presup_exp_eq_prop_eq_var1 : mctt. Lemma presup_exp_eq_prop_eq_wf : forall {Γ i A}, {{ Γ ⊢ A : Type@i }} -> @@ -356,7 +356,7 @@ Proof. Qed. #[export] -Hint Resolve presup_exp_eq_prop_eq_wf : mcltt. +Hint Resolve presup_exp_eq_prop_eq_wf : mctt. Lemma presup_exp_eq_prop_eq_sub_helper2 : forall {Γ σ Δ i A M1 M2}, {{ Γ ⊢s σ : Δ }} -> @@ -377,7 +377,7 @@ Proof. Qed. #[export] -Hint Resolve presup_exp_eq_prop_eq_sub_helper2 : mcltt. +Hint Resolve presup_exp_eq_prop_eq_sub_helper2 : mctt. Lemma presup_exp_eq_prop_eq_typ_sub2_eq : forall {Γ σ Δ i A M1 M2}, {{ Γ ⊢s σ : Δ }} -> @@ -407,7 +407,7 @@ Proof. Qed. #[export] -Hint Resolve presup_exp_eq_prop_eq_typ_sub2_eq : mcltt. +Hint Resolve presup_exp_eq_prop_eq_typ_sub2_eq : mctt. Lemma presup_exp_eq_prop_eq_sub_helper3 : forall {Γ σ Δ i A M1 M2 N}, {{ Γ ⊢s σ : Δ }} -> @@ -426,7 +426,7 @@ Proof. Qed. #[export] -Hint Resolve presup_exp_eq_prop_eq_sub_helper3 : mcltt. +Hint Resolve presup_exp_eq_prop_eq_sub_helper3 : mctt. Lemma presup_exp_eq_prop_eq_id_sub_helper2 : forall {Γ i A M1 M2}, {{ Γ ⊢ A : Type@i }} -> @@ -447,7 +447,7 @@ Proof. Qed. #[export] -Hint Resolve presup_exp_eq_prop_eq_id_sub_helper2 : mcltt. +Hint Resolve presup_exp_eq_prop_eq_id_sub_helper2 : mctt. Lemma presup_exp_eq_prop_eq_typ_id_sub2_eq : forall {Γ i A M1 M2}, {{ Γ ⊢ A : Type@i }} -> @@ -472,7 +472,7 @@ Proof. Qed. #[export] -Hint Resolve presup_exp_eq_prop_eq_typ_id_sub2_eq : mcltt. +Hint Resolve presup_exp_eq_prop_eq_typ_id_sub2_eq : mctt. Lemma presup_exp_eq_prop_eq_id_sub_helper3 : forall {Γ i A M1 M2 N}, {{ Γ ⊢ A : Type@i }} -> @@ -490,7 +490,7 @@ Proof. Qed. #[export] -Hint Resolve presup_exp_eq_prop_eq_id_sub_helper3 : mcltt. +Hint Resolve presup_exp_eq_prop_eq_id_sub_helper3 : mctt. Lemma presup_exp_eq_refl_sub_right : forall {Γ σ Δ i A M}, {{ ⊢ Γ }} -> @@ -509,7 +509,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_refl_sub_right : mcltt. +Hint Resolve presup_exp_eq_refl_sub_right : mctt. Lemma presup_exp_eq_eqrec_sub_left : forall {Γ σ Δ i A M1 M2 j B N BR}, {{ ⊢ Γ }} -> @@ -554,7 +554,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_eqrec_sub_left : mcltt. +Hint Resolve presup_exp_eq_eqrec_sub_left : mctt. Lemma presup_exp_eq_eqrec_sub_right : forall {Γ σ Δ i A M1 M2 j B N BR}, {{ ⊢ Γ }} -> @@ -881,7 +881,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_eqrec_sub_right : mcltt. +Hint Resolve presup_exp_eq_eqrec_sub_right : mctt. Lemma presup_exp_eq_refl_cong_right : forall {Γ i A A' M M'}, {{ ⊢ Γ }} -> @@ -899,7 +899,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_refl_cong_right : mcltt. +Hint Resolve presup_exp_eq_refl_cong_right : mctt. Lemma presup_exp_eq_eqrec_cong_right : forall {Γ i A A' M1 M1' M2 M2' j B B' BR BR' N N'}, {{ ⊢ Γ }} -> @@ -1029,7 +1029,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_eqrec_cong_right : mcltt. +Hint Resolve presup_exp_eq_eqrec_cong_right : mctt. Lemma presup_exp_eq_eqrec_beta_right : forall {Γ i A M j B BR}, {{ ⊢ Γ }} -> @@ -1137,7 +1137,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_eqrec_beta_right : mcltt. +Hint Resolve presup_exp_eq_eqrec_beta_right : mctt. Lemma presup_exp_eq_var_0_sub_left : forall {Γ σ Δ i A M}, {{ ⊢ Γ }} -> @@ -1154,7 +1154,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_var_0_sub_left : mcltt. +Hint Resolve presup_exp_eq_var_0_sub_left : mctt. Lemma presup_exp_eq_var_S_sub_left : forall {Γ σ Δ i A M B x}, {{ ⊢ Γ }} -> @@ -1173,7 +1173,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_var_S_sub_left : mcltt. +Hint Resolve presup_exp_eq_var_S_sub_left : mctt. Lemma presup_exp_eq_sub_cong_right : forall {Γ σ σ' Δ i A M M'}, {{ ⊢ Δ }} -> @@ -1193,7 +1193,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_sub_cong_right : mcltt. +Hint Resolve presup_exp_eq_sub_cong_right : mctt. Lemma presup_exp_eq_sub_compose_right : forall {Γ τ Γ' σ Γ'' i A M}, {{ ⊢ Γ }} -> @@ -1210,7 +1210,7 @@ Proof. Qed. #[local] -Hint Resolve presup_exp_eq_sub_compose_right : mcltt. +Hint Resolve presup_exp_eq_sub_compose_right : mctt. #[local] Ltac gen_presup_IH presup_exp_eq presup_sub_eq presup_subtyp H := diff --git a/theories/Core/Syntactic/Syntax.v b/theories/Core/Syntactic/Syntax.v index af77db0..97b8540 100644 --- a/theories/Core/Syntactic/Syntax.v +++ b/theories/Core/Syntactic/Syntax.v @@ -1,6 +1,6 @@ From Coq Require Import List String. -From Mcltt.Core Require Import Base. +From Mctt.Core Require Import Base. (** * Concrete Syntax Tree *) Module Cst. @@ -134,62 +134,62 @@ Arguments q σ/. #[global] Declare Custom Entry exp. #[global] Declare Custom Entry nf. -#[global] Bind Scope mcltt_scope with exp. -#[global] Bind Scope mcltt_scope with sub. -#[global] Bind Scope mcltt_scope with nf. -#[global] Bind Scope mcltt_scope with ne. -Open Scope mcltt_scope. +#[global] Bind Scope mctt_scope with exp. +#[global] Bind Scope mctt_scope with sub. +#[global] Bind Scope mctt_scope with nf. +#[global] Bind Scope mctt_scope with ne. +Open Scope mctt_scope. (** ** Syntactic Notations *) Module Syntax_Notations. (** We need to define substitution notation first to assert [left associativity] of level 0. *) - Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, e custom exp, s custom exp at level 60, left associativity, format "e [ s ]") : mcltt_scope. - - Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{' x '}}}'") : mcltt_scope. - Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : mcltt_scope. - Notation "'^' x" := x (in custom exp at level 0, x constr at level 0) : mcltt_scope. - Notation "x" := x (in custom exp at level 0, x ident) : mcltt_scope. - - Notation "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0, format "'Type' @ n") : mcltt_scope. - Notation "'ℕ'" := a_nat (in custom exp) : mcltt_scope. - Notation "'zero'" := a_zero (in custom exp at level 0) : mcltt_scope. - Notation "'succ' e" := (a_succ e) (in custom exp at level 1, e custom exp at level 0) : mcltt_scope. - Notation "'rec' e 'return' A | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec A ez es e) (in custom exp at level 0, A custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : mcltt_scope. - Notation "'Π' A B" := (a_pi A B) (in custom exp at level 1, A custom exp at level 0, B custom exp at level 60) : mcltt_scope. - Notation "'λ' A e" := (a_fn A e) (in custom exp at level 1, A custom exp at level 0, e custom exp at level 60) : mcltt_scope. - Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : mcltt_scope. - Notation "'Eq' A M N" := (a_eq A M N) (in custom exp at level 1, A custom exp at level 30, M custom exp at level 35, N custom exp at level 40) : mcltt_scope. - Notation "'refl' A M" := (a_refl A M) (in custom exp at level 1, A custom exp at level 30, M custom exp at level 40) : mcltt_scope. - Notation "'eqrec' N 'as' 'Eq' A M1 M2 'return' B | 'refl' -> BR 'end'" := (a_eqrec A B BR M1 M2 N) (in custom exp at level 0, A custom exp at level 30, B custom exp at level 60, BR custom exp at level 60, M1 custom exp at level 35, M2 custom exp at level 40, N custom exp at level 60) : mcltt_scope. - - Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0, format "'#' n") : mcltt_scope. - - Notation "'Id'" := a_id (in custom exp at level 0) : mcltt_scope. - Notation "'Wk'" := a_weaken (in custom exp at level 0) : mcltt_scope. - Notation "σ ∘ τ" := (a_compose σ τ) (in custom exp at level 40, right associativity, format "σ ∘ τ") : mcltt_scope. - Notation "σ ,, e" := (a_extend σ e) (in custom exp at level 50, left associativity, format "σ ,, e") : mcltt_scope. - Notation "'q' σ" := (q σ) (in custom exp at level 30) : mcltt_scope. - - Notation "⋅" := nil (in custom exp at level 0) : mcltt_scope. - Notation "x , y" := (cons y x) (in custom exp at level 50, left associativity, format "x , y") : mcltt_scope. - - Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{' x '}}}'") : mcltt_scope. - Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : mcltt_scope. - Notation "'^' x" := x (in custom nf at level 0, x constr at level 0) : mcltt_scope. - Notation "x" := x (in custom nf at level 0, x ident) : mcltt_scope. - - Notation "'Type' @ n" := (nf_typ n) (in custom nf at level 0, n constr at level 0, format "'Type' @ n") : mcltt_scope. - Notation "'ℕ'" := nf_nat (in custom nf) : mcltt_scope. - Notation "'zero'" := nf_zero (in custom nf at level 0) : mcltt_scope. - Notation "'succ' M" := (nf_succ M) (in custom nf at level 2, M custom nf at level 1) : mcltt_scope. - Notation "'rec' M 'return' A | 'zero' -> MZ | 'succ' -> MS 'end'" := (ne_natrec A MZ MS M) (in custom nf at level 0, A custom nf at level 60, MZ custom nf at level 60, MS custom nf at level 60, M custom nf at level 60) : mcltt_scope. - Notation "'Π' A B" := (nf_pi A B) (in custom nf at level 2, A custom nf at level 1, B custom nf at level 60) : mcltt_scope. - Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 2, A custom nf at level 1, e custom nf at level 60) : mcltt_scope. - Notation "f x .. y" := (ne_app .. (ne_app f x) .. y) (in custom nf at level 40, f custom nf, x custom nf at next level, y custom nf at next level) : mcltt_scope. - Notation "'Eq' A M N" := (nf_eq A M N) (in custom nf at level 1, A custom nf at level 30, M custom nf at level 35, N custom nf at level 40) : mcltt_scope. - Notation "'refl' A M" := (nf_refl A M) (in custom nf at level 1, A custom nf at level 30, M custom nf at level 40) : mcltt_scope. - Notation "'eqrec' N 'as' 'Eq' A M1 M2 'return' B | 'refl' -> BR 'end'" := (ne_eqrec A B BR M1 M2 N) (in custom nf at level 0, A custom nf at level 30, B custom nf at level 60, BR custom nf at level 60, M1 custom nf at level 35, M2 custom nf at level 40, N custom nf at level 60) : mcltt_scope. - - Notation "'#' n" := (ne_var n) (in custom nf at level 0, n constr at level 0, format "'#' n") : mcltt_scope. - Notation "'⇑' M" := (nf_neut M) (in custom nf at level 0, M custom nf at level 99, format "'⇑' M") : mcltt_scope. + Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, e custom exp, s custom exp at level 60, left associativity, format "e [ s ]") : mctt_scope. + + Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{' x '}}}'") : mctt_scope. + Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : mctt_scope. + Notation "'^' x" := x (in custom exp at level 0, x constr at level 0) : mctt_scope. + Notation "x" := x (in custom exp at level 0, x ident) : mctt_scope. + + Notation "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0, format "'Type' @ n") : mctt_scope. + Notation "'ℕ'" := a_nat (in custom exp) : mctt_scope. + Notation "'zero'" := a_zero (in custom exp at level 0) : mctt_scope. + Notation "'succ' e" := (a_succ e) (in custom exp at level 1, e custom exp at level 0) : mctt_scope. + Notation "'rec' e 'return' A | 'zero' -> ez | 'succ' -> es 'end'" := (a_natrec A ez es e) (in custom exp at level 0, A custom exp at level 60, ez custom exp at level 60, es custom exp at level 60, e custom exp at level 60) : mctt_scope. + Notation "'Π' A B" := (a_pi A B) (in custom exp at level 1, A custom exp at level 0, B custom exp at level 60) : mctt_scope. + Notation "'λ' A e" := (a_fn A e) (in custom exp at level 1, A custom exp at level 0, e custom exp at level 60) : mctt_scope. + Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : mctt_scope. + Notation "'Eq' A M N" := (a_eq A M N) (in custom exp at level 1, A custom exp at level 30, M custom exp at level 35, N custom exp at level 40) : mctt_scope. + Notation "'refl' A M" := (a_refl A M) (in custom exp at level 1, A custom exp at level 30, M custom exp at level 40) : mctt_scope. + Notation "'eqrec' N 'as' 'Eq' A M1 M2 'return' B | 'refl' -> BR 'end'" := (a_eqrec A B BR M1 M2 N) (in custom exp at level 0, A custom exp at level 30, B custom exp at level 60, BR custom exp at level 60, M1 custom exp at level 35, M2 custom exp at level 40, N custom exp at level 60) : mctt_scope. + + Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0, format "'#' n") : mctt_scope. + + Notation "'Id'" := a_id (in custom exp at level 0) : mctt_scope. + Notation "'Wk'" := a_weaken (in custom exp at level 0) : mctt_scope. + Notation "σ ∘ τ" := (a_compose σ τ) (in custom exp at level 40, right associativity, format "σ ∘ τ") : mctt_scope. + Notation "σ ,, e" := (a_extend σ e) (in custom exp at level 50, left associativity, format "σ ,, e") : mctt_scope. + Notation "'q' σ" := (q σ) (in custom exp at level 30) : mctt_scope. + + Notation "⋅" := nil (in custom exp at level 0) : mctt_scope. + Notation "x , y" := (cons y x) (in custom exp at level 50, left associativity, format "x , y") : mctt_scope. + + Notation "n{{{ x }}}" := x (at level 0, x custom nf at level 99, format "'n{{{' x '}}}'") : mctt_scope. + Notation "( x )" := x (in custom nf at level 0, x custom nf at level 60) : mctt_scope. + Notation "'^' x" := x (in custom nf at level 0, x constr at level 0) : mctt_scope. + Notation "x" := x (in custom nf at level 0, x ident) : mctt_scope. + + Notation "'Type' @ n" := (nf_typ n) (in custom nf at level 0, n constr at level 0, format "'Type' @ n") : mctt_scope. + Notation "'ℕ'" := nf_nat (in custom nf) : mctt_scope. + Notation "'zero'" := nf_zero (in custom nf at level 0) : mctt_scope. + Notation "'succ' M" := (nf_succ M) (in custom nf at level 2, M custom nf at level 1) : mctt_scope. + Notation "'rec' M 'return' A | 'zero' -> MZ | 'succ' -> MS 'end'" := (ne_natrec A MZ MS M) (in custom nf at level 0, A custom nf at level 60, MZ custom nf at level 60, MS custom nf at level 60, M custom nf at level 60) : mctt_scope. + Notation "'Π' A B" := (nf_pi A B) (in custom nf at level 2, A custom nf at level 1, B custom nf at level 60) : mctt_scope. + Notation "'λ' A e" := (nf_fn A e) (in custom nf at level 2, A custom nf at level 1, e custom nf at level 60) : mctt_scope. + Notation "f x .. y" := (ne_app .. (ne_app f x) .. y) (in custom nf at level 40, f custom nf, x custom nf at next level, y custom nf at next level) : mctt_scope. + Notation "'Eq' A M N" := (nf_eq A M N) (in custom nf at level 1, A custom nf at level 30, M custom nf at level 35, N custom nf at level 40) : mctt_scope. + Notation "'refl' A M" := (nf_refl A M) (in custom nf at level 1, A custom nf at level 30, M custom nf at level 40) : mctt_scope. + Notation "'eqrec' N 'as' 'Eq' A M1 M2 'return' B | 'refl' -> BR 'end'" := (ne_eqrec A B BR M1 M2 N) (in custom nf at level 0, A custom nf at level 30, B custom nf at level 60, BR custom nf at level 60, M1 custom nf at level 35, M2 custom nf at level 40, N custom nf at level 60) : mctt_scope. + + Notation "'#' n" := (ne_var n) (in custom nf at level 0, n constr at level 0, format "'#' n") : mctt_scope. + Notation "'⇑' M" := (nf_neut M) (in custom nf at level 0, M custom nf at level 99, format "'⇑' M") : mctt_scope. End Syntax_Notations. diff --git a/theories/Core/Syntactic/System.v b/theories/Core/Syntactic/System.v index 29464f7..45a0c2c 100644 --- a/theories/Core/Syntactic/System.v +++ b/theories/Core/Syntactic/System.v @@ -1 +1 @@ -From Mcltt.Core.Syntactic.System Require Export Definitions Lemmas Tactics. +From Mctt.Core.Syntactic.System Require Export Definitions Lemmas Tactics. diff --git a/theories/Core/Syntactic/System/Definitions.v b/theories/Core/Syntactic/System/Definitions.v index cc6ede0..650a9f9 100644 --- a/theories/Core/Syntactic/System/Definitions.v +++ b/theories/Core/Syntactic/System/Definitions.v @@ -1,8 +1,8 @@ From Coq Require Import List Classes.RelationClasses Setoid Morphisms. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic Require Export Syntax. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic Require Export Syntax. Import Syntax_Notations. Reserved Notation "⊢ Γ" (in custom judg at level 80, Γ custom exp). @@ -464,7 +464,7 @@ Inductive wf_ctx_eq : ctx -> ctx -> Prop := where "⊢ Γ ≈ Γ'" := (wf_ctx_eq Γ Γ') (in custom judg) : type_scope. #[export] -Hint Constructors wf_ctx wf_ctx_eq wf_ctx_sub wf_exp wf_sub wf_exp_eq wf_sub_eq wf_subtyp ctx_lookup : mcltt. +Hint Constructors wf_ctx wf_ctx_eq wf_ctx_sub wf_exp wf_sub wf_exp_eq wf_sub_eq wf_subtyp ctx_lookup : mctt. #[export] Instance wf_exp_eq_PER Γ A : PER (wf_exp_eq Γ A). @@ -502,7 +502,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve presup_ctx_sub : mcltt. +Hint Resolve presup_ctx_sub : mctt. Lemma presup_ctx_sub_left : forall {Γ Δ}, {{ ⊢ Γ ⊆ Δ }} -> {{ ⊢ Γ }}. Proof with easy. @@ -510,7 +510,7 @@ Proof with easy. Qed. #[export] -Hint Resolve presup_ctx_sub_left : mcltt. +Hint Resolve presup_ctx_sub_left : mctt. Lemma presup_ctx_sub_right : forall {Γ Δ}, {{ ⊢ Γ ⊆ Δ }} -> {{ ⊢ Δ }}. Proof with easy. @@ -518,7 +518,7 @@ Proof with easy. Qed. #[export] -Hint Resolve presup_ctx_sub_right : mcltt. +Hint Resolve presup_ctx_sub_right : mctt. Lemma presup_subtyp_right : forall {Γ A B}, {{ Γ ⊢ A ⊆ B }} -> exists i, {{ Γ ⊢ B : Type@i }}. Proof with mautosolve. @@ -526,7 +526,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve presup_subtyp_right : mcltt. +Hint Resolve presup_subtyp_right : mctt. (** Subtyping Rules without Extra Arguments *) @@ -541,9 +541,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_subtyp' : mcltt. +Hint Resolve wf_exp_subtyp' : mctt. #[export] -Remove Hints wf_exp_subtyp : mcltt. +Remove Hints wf_exp_subtyp : mctt. Lemma wf_sub_subtyp' : forall Γ Δ Δ' σ, {{ Γ ⊢s σ : Δ }} -> @@ -555,9 +555,9 @@ Proof. Qed. #[export] -Hint Resolve wf_sub_subtyp' : mcltt. +Hint Resolve wf_sub_subtyp' : mctt. #[export] -Remove Hints wf_sub_subtyp : mcltt. +Remove Hints wf_sub_subtyp : mctt. Lemma wf_exp_eq_subtyp' : forall Γ A A' M M', {{ Γ ⊢ M ≈ M' : A }} -> @@ -570,9 +570,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_subtyp' : mcltt. +Hint Resolve wf_exp_eq_subtyp' : mctt. #[export] -Remove Hints wf_exp_eq_subtyp : mcltt. +Remove Hints wf_exp_eq_subtyp : mctt. Lemma wf_sub_eq_subtyp' : forall Γ Δ Δ' σ σ', {{ Γ ⊢s σ ≈ σ' : Δ }} -> @@ -584,9 +584,9 @@ Proof. Qed. #[export] -Hint Resolve wf_sub_eq_subtyp' : mcltt. +Hint Resolve wf_sub_eq_subtyp' : mctt. #[export] -Remove Hints wf_sub_eq_subtyp : mcltt. +Remove Hints wf_sub_eq_subtyp : mctt. Add Parametric Morphism Γ T : (wf_exp_eq Γ T) with signature wf_exp_eq Γ T ==> eq ==> iff as wf_exp_eq_morphism_iff1. @@ -613,15 +613,15 @@ Proof. Qed. #[export] -Hint Rewrite -> wf_exp_eq_typ_sub wf_exp_eq_nat_sub wf_exp_eq_eq_sub using mauto 3 : mcltt. +Hint Rewrite -> wf_exp_eq_typ_sub wf_exp_eq_nat_sub wf_exp_eq_eq_sub using mauto 3 : mctt. #[export] Hint Rewrite -> wf_sub_eq_id_compose_right wf_sub_eq_id_compose_left wf_sub_eq_compose_assoc (* prefer right association *) - wf_sub_eq_p_extend using mauto 4 : mcltt. + wf_sub_eq_p_extend using mauto 4 : mctt. #[export] -Hint Rewrite -> wf_exp_eq_sub_id wf_exp_eq_pi_sub using mauto 4 : mcltt. +Hint Rewrite -> wf_exp_eq_sub_id wf_exp_eq_pi_sub using mauto 4 : mctt. #[export] Instance wf_exp_eq_per_elem Γ T : PERElem _ (wf_exp Γ T) (wf_exp_eq Γ T). diff --git a/theories/Core/Syntactic/System/Lemmas.v b/theories/Core/Syntactic/System/Lemmas.v index eddb871..faeaf3a 100644 --- a/theories/Core/Syntactic/System/Lemmas.v +++ b/theories/Core/Syntactic/System/Lemmas.v @@ -1,6 +1,6 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic.System Require Import Definitions. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic.System Require Import Definitions. Import Syntax_Notations. (** ** Basic Context Properties *) @@ -12,7 +12,7 @@ Proof. induction 1; simpl; lia. Qed. #[export] -Hint Resolve ctx_lookup_lt : mcltt. +Hint Resolve ctx_lookup_lt : mctt. Lemma functional_ctx_lookup : forall {Γ A A' x}, {{ #x : A ∈ Γ }} -> @@ -30,7 +30,10 @@ Proof with now eauto. inversion 1... Qed. -Corollary ctx_decomp_left : forall {Γ A}, {{ ⊢ Γ, A }} -> {{ ⊢ Γ }}. +#[export] +Hint Resolve ctx_decomp : mctt. + +Corollary ctx_decomp_left : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }}. Proof with easy. intros * ?%ctx_decomp... Qed. @@ -41,7 +44,7 @@ Proof with easy. Qed. #[export] -Hint Resolve ctx_decomp_left ctx_decomp_right : mcltt. +Hint Resolve ctx_decomp_left ctx_decomp_right : mctt. (** ** Core Presuppositions *) @@ -63,7 +66,7 @@ Proof with easy. Qed. #[export] -Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mcltt. +Hint Resolve presup_ctx_eq presup_ctx_eq_left presup_ctx_eq_right : mctt. Lemma presup_sub : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} /\ {{ ⊢ Δ }}. Proof with mautosolve. @@ -81,7 +84,7 @@ Proof with easy. Qed. #[export] -Hint Resolve presup_sub presup_sub_left presup_sub_right : mcltt. +Hint Resolve presup_sub presup_sub_left presup_sub_right : mctt. (** With [presup_sub], we can prove similar for [exp]. *) @@ -91,7 +94,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve presup_exp_ctx : mcltt. +Hint Resolve presup_exp_ctx : mctt. (** and other presuppositions about context well-formedness. *) @@ -111,7 +114,7 @@ Proof with easy. Qed. #[export] -Hint Resolve presup_sub_eq_ctx presup_sub_eq_ctx_left presup_sub_eq_ctx_right : mcltt. +Hint Resolve presup_sub_eq_ctx presup_sub_eq_ctx_left presup_sub_eq_ctx_right : mctt. Lemma presup_exp_eq_ctx : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }}. Proof with mautosolve 2. @@ -119,7 +122,7 @@ Proof with mautosolve 2. Qed. #[export] -Hint Resolve presup_exp_eq_ctx : mcltt. +Hint Resolve presup_exp_eq_ctx : mctt. (** *** Immediate Results of Context Presuppositions *) @@ -143,7 +146,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve wf_cumu wf_exp_eq_cumu : mcltt. +Hint Resolve wf_cumu wf_exp_eq_cumu : mctt. Lemma wf_ctx_sub_refl : forall Γ Δ, {{ ⊢ Γ ≈ Δ }} -> @@ -151,7 +154,7 @@ Lemma wf_ctx_sub_refl : forall Γ Δ, Proof. induction 1; mauto. Qed. #[export] -Hint Resolve wf_ctx_sub_refl : mcltt. +Hint Resolve wf_ctx_sub_refl : mctt. Lemma wf_conv : forall Γ M A i A', {{ Γ ⊢ M : A }} -> @@ -162,7 +165,7 @@ Lemma wf_conv : forall Γ M A i A', Proof. mauto. Qed. #[export] -Hint Resolve wf_conv : mcltt. +Hint Resolve wf_conv : mctt. Lemma wf_sub_conv : forall Γ σ Δ Δ', {{ Γ ⊢s σ : Δ }} -> @@ -171,7 +174,7 @@ Lemma wf_sub_conv : forall Γ σ Δ Δ', Proof. mauto. Qed. #[export] -Hint Resolve wf_sub_conv : mcltt. +Hint Resolve wf_sub_conv : mctt. Lemma wf_exp_eq_conv : forall Γ M M' A A' i, {{ Γ ⊢ M ≈ M' : A }} -> @@ -182,7 +185,7 @@ Lemma wf_exp_eq_conv : forall Γ M M' A A' i, Proof. mauto. Qed. #[export] -Hint Resolve wf_exp_eq_conv : mcltt. +Hint Resolve wf_exp_eq_conv : mctt. Lemma wf_sub_eq_conv : forall Γ σ σ' Δ Δ', {{ Γ ⊢s σ ≈ σ' : Δ }} -> @@ -191,7 +194,7 @@ Lemma wf_sub_eq_conv : forall Γ σ σ' Δ Δ', Proof. mauto. Qed. #[export] -Hint Resolve wf_sub_eq_conv : mcltt. +Hint Resolve wf_sub_eq_conv : mctt. Add Parametric Morphism Γ : (wf_sub_eq Γ) with signature wf_ctx_eq ==> eq ==> eq ==> iff as wf_sub_eq_morphism_iff3. @@ -210,7 +213,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve lift_exp_ge : mcltt. +Hint Resolve lift_exp_ge : mctt. Corollary lift_exp_max_left : forall {Γ A n} m, {{ Γ ⊢ A : Type@n }} -> @@ -237,7 +240,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve lift_exp_eq_ge : mcltt. +Hint Resolve lift_exp_eq_ge : mctt. Corollary lift_exp_eq_max_left : forall {Γ A A' n} m, {{ Γ ⊢ A ≈ A' : Type@n }} -> @@ -263,7 +266,7 @@ Lemma exp_eq_refl : forall {Γ M A}, Proof. mauto. Qed. #[export] -Hint Resolve exp_eq_refl : mcltt. +Hint Resolve exp_eq_refl : mctt. Lemma exp_eq_trans_typ_max : forall {Γ i i' A A' A''}, {{ Γ ⊢ A ≈ A' : Type@i }} -> @@ -276,7 +279,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_trans_typ_max : mcltt. +Hint Resolve exp_eq_trans_typ_max : mctt. Lemma sub_eq_refl : forall {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> @@ -284,7 +287,7 @@ Lemma sub_eq_refl : forall {Γ σ Δ}, Proof. mauto. Qed. #[export] -Hint Resolve sub_eq_refl : mcltt. +Hint Resolve sub_eq_refl : mctt. Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> @@ -294,7 +297,7 @@ Proof. Qed. #[export] -Hint Resolve ctx_eq_refl : mcltt. +Hint Resolve ctx_eq_refl : mctt. (** *** Lemmas for [exp] of [{{{ Type@i }}}] *) @@ -309,7 +312,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve exp_sub_typ : mcltt. +Hint Resolve exp_sub_typ : mctt. Lemma presup_ctx_lookup_typ : forall {Γ A x}, {{ ⊢ Γ }} -> @@ -323,7 +326,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve presup_ctx_lookup_typ : mcltt. +Hint Resolve presup_ctx_lookup_typ : mctt. Lemma exp_eq_sub_cong_typ1 : forall {Δ Γ A A' σ i}, {{ Δ ⊢ A ≈ A' : Type@i }} -> @@ -355,7 +358,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve exp_eq_sub_cong_typ1 exp_eq_sub_cong_typ2' exp_eq_sub_compose_typ : mcltt. +Hint Resolve exp_eq_sub_cong_typ1 exp_eq_sub_cong_typ2' exp_eq_sub_compose_typ : mctt. Lemma exp_eq_sub_compose_weaken_extend_typ : forall {Γ σ Δ i A j B M}, {{ Γ ⊢s σ : Δ }} -> @@ -371,7 +374,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve exp_eq_sub_compose_weaken_extend_typ : mcltt. +Hint Resolve exp_eq_sub_compose_weaken_extend_typ : mctt. Lemma exp_eq_sub_compose_weaken_id_extend_typ : forall {Γ i A j B M}, {{ Γ ⊢ A : Type@i }} -> @@ -387,7 +390,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_sub_compose_weaken_id_extend_typ : mcltt. +Hint Resolve exp_eq_sub_compose_weaken_id_extend_typ : mctt. Lemma exp_eq_sub_compose_double_weaken_double_extend_typ : forall {Γ σ Δ i A j B M k C N}, {{ Γ ⊢s σ : Δ }} -> @@ -406,7 +409,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_sub_compose_double_weaken_double_extend_typ : mcltt. +Hint Resolve exp_eq_sub_compose_double_weaken_double_extend_typ : mctt. Lemma exp_eq_sub_compose_double_weaken_id_double_extend_typ : forall {Γ i A j B M k C N}, {{ Γ ⊢ A : Type@i }} -> @@ -424,7 +427,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_sub_compose_double_weaken_id_double_extend_typ : mcltt. +Hint Resolve exp_eq_sub_compose_double_weaken_id_double_extend_typ : mctt. Lemma exp_eq_typ_sub_sub : forall {Γ Δ Ψ σ τ i}, {{ Δ ⊢s σ : Ψ }} -> @@ -433,9 +436,9 @@ Lemma exp_eq_typ_sub_sub : forall {Γ Δ Ψ σ τ i}, Proof. mauto. Qed. #[export] -Hint Resolve exp_eq_typ_sub_sub : mcltt. +Hint Resolve exp_eq_typ_sub_sub : mctt. #[export] -Hint Rewrite -> @exp_eq_sub_compose_typ @exp_eq_typ_sub_sub using mauto 4 : mcltt. +Hint Rewrite -> @exp_eq_sub_compose_typ @exp_eq_typ_sub_sub using mauto 4 : mctt. Lemma vlookup_0_typ : forall {Γ i}, {{ ⊢ Γ }} -> @@ -457,7 +460,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve vlookup_0_typ vlookup_1_typ : mcltt. +Hint Resolve vlookup_0_typ vlookup_1_typ : mctt. Lemma exp_sub_typ_helper : forall {Γ σ Δ M i}, {{ Γ ⊢s σ : Δ }} -> @@ -469,7 +472,7 @@ Proof. Qed. #[export] -Hint Resolve exp_sub_typ_helper : mcltt. +Hint Resolve exp_sub_typ_helper : mctt. Lemma exp_eq_var_0_sub_typ : forall {Γ σ Δ M i}, {{ Γ ⊢s σ : Δ }} -> @@ -495,9 +498,9 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_var_0_sub_typ exp_eq_var_1_sub_typ : mcltt. +Hint Resolve exp_eq_var_0_sub_typ exp_eq_var_1_sub_typ : mctt. #[export] -Hint Rewrite -> @exp_eq_var_0_sub_typ @exp_eq_var_1_sub_typ : mcltt. +Hint Rewrite -> @exp_eq_var_0_sub_typ @exp_eq_var_1_sub_typ : mctt. Lemma exp_eq_var_0_weaken_typ : forall {Γ A i}, {{ ⊢ Γ, A }} -> @@ -513,7 +516,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve exp_eq_var_0_weaken_typ : mcltt. +Hint Resolve exp_eq_var_0_weaken_typ : mctt. Lemma sub_extend_typ : forall {Γ σ Δ M i}, {{ Γ ⊢s σ : Δ }} -> @@ -525,7 +528,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_extend_typ : mcltt. +Hint Resolve sub_extend_typ : mctt. Lemma sub_eq_extend_cong_typ : forall {Γ σ σ' Δ M M' i}, {{ Γ ⊢s σ : Δ }} -> @@ -560,7 +563,8 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_eq_extend_cong_typ sub_eq_extend_compose_typ sub_eq_p_extend_typ : mcltt. +Hint Resolve sub_eq_extend_cong_typ sub_eq_extend_compose_typ sub_eq_p_extend_typ : mctt. + Lemma exp_eq_sub_sub_compose_cong_typ : forall {Γ Δ Δ' Ψ σ τ σ' τ' A i}, {{ Ψ ⊢ A : Type@i }} -> @@ -578,7 +582,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_sub_sub_compose_cong_typ : mcltt. +Hint Resolve exp_eq_sub_sub_compose_cong_typ : mctt. (** *** Lemmas for [exp] of [{{{ ℕ }}}] *) @@ -593,7 +597,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve exp_sub_nat : mcltt. +Hint Resolve exp_sub_nat : mctt. Lemma exp_eq_sub_cong_nat1 : forall {Δ Γ M M' σ}, {{ Δ ⊢ M ≈ M' : ℕ }} -> @@ -625,7 +629,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_sub_nat exp_eq_sub_cong_nat1 exp_eq_sub_cong_nat2 exp_eq_sub_compose_nat : mcltt. +Hint Resolve exp_sub_nat exp_eq_sub_cong_nat1 exp_eq_sub_cong_nat2 exp_eq_sub_compose_nat : mctt. Lemma exp_eq_nat_sub_sub : forall {Γ Δ Ψ σ τ}, {{ Δ ⊢s σ : Ψ }} -> @@ -634,7 +638,7 @@ Lemma exp_eq_nat_sub_sub : forall {Γ Δ Ψ σ τ}, Proof. mauto. Qed. #[export] -Hint Resolve exp_eq_nat_sub_sub : mcltt. +Hint Resolve exp_eq_nat_sub_sub : mctt. Lemma exp_eq_nat_sub_sub_to_nat_sub : forall {Γ Δ Ψ Ψ' σ τ σ'}, {{ Δ ⊢s σ : Ψ }} -> @@ -644,7 +648,7 @@ Lemma exp_eq_nat_sub_sub_to_nat_sub : forall {Γ Δ Ψ Ψ' σ τ σ'}, Proof. mauto. Qed. #[export] -Hint Resolve exp_eq_nat_sub_sub_to_nat_sub : mcltt. +Hint Resolve exp_eq_nat_sub_sub_to_nat_sub : mctt. Lemma exp_eq_sub_compose_weaken_extend_nat : forall {Γ σ Δ M i B N}, {{ Γ ⊢s σ : Δ }} -> @@ -660,7 +664,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve exp_eq_sub_compose_weaken_extend_nat : mcltt. +Hint Resolve exp_eq_sub_compose_weaken_extend_nat : mctt. Lemma exp_eq_sub_compose_weaken_id_extend_nat : forall {Γ M i B N}, {{ Γ ⊢ M : ℕ }} -> @@ -676,7 +680,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_sub_compose_weaken_id_extend_nat : mcltt. +Hint Resolve exp_eq_sub_compose_weaken_id_extend_nat : mctt. Lemma exp_eq_sub_compose_double_weaken_double_extend_nat : forall {Γ σ Δ M i B N j C L}, {{ Γ ⊢s σ : Δ }} -> @@ -695,7 +699,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_sub_compose_double_weaken_double_extend_nat : mcltt. +Hint Resolve exp_eq_sub_compose_double_weaken_double_extend_nat : mctt. Lemma exp_eq_sub_compose_double_weaken_id_double_extend_nat : forall {Γ M i B N j C L}, {{ Γ ⊢ M : ℕ }} -> @@ -713,7 +717,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_sub_compose_double_weaken_id_double_extend_nat : mcltt. +Hint Resolve exp_eq_sub_compose_double_weaken_id_double_extend_nat : mctt. Lemma vlookup_0_nat : forall {Γ}, {{ ⊢ Γ }} -> @@ -735,7 +739,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve vlookup_0_nat vlookup_1_nat : mcltt. +Hint Resolve vlookup_0_nat vlookup_1_nat : mctt. Lemma exp_sub_nat_helper : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> @@ -747,7 +751,7 @@ Proof. Qed. #[export] -Hint Resolve exp_sub_nat_helper : mcltt. +Hint Resolve exp_sub_nat_helper : mctt. Lemma exp_eq_var_0_sub_nat : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> @@ -772,7 +776,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_var_0_sub_nat exp_eq_var_1_sub_nat : mcltt. +Hint Resolve exp_eq_var_0_sub_nat exp_eq_var_1_sub_nat : mctt. Lemma exp_eq_var_0_weaken_nat : forall {Γ A}, {{ ⊢ Γ, A }} -> @@ -786,7 +790,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_var_0_weaken_nat : mcltt. +Hint Resolve exp_eq_var_0_weaken_nat : mctt. Lemma sub_extend_nat : forall {Γ σ Δ M}, {{ Γ ⊢s σ : Δ }} -> @@ -798,7 +802,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve sub_extend_nat : mcltt. +Hint Resolve sub_extend_nat : mctt. Lemma sub_eq_extend_cong_nat : forall {Γ σ σ' Δ M M'}, {{ Γ ⊢s σ : Δ }} -> @@ -832,7 +836,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve sub_eq_extend_cong_nat sub_eq_extend_compose_nat sub_eq_p_extend_nat : mcltt. +Hint Resolve sub_eq_extend_cong_nat sub_eq_extend_compose_nat sub_eq_p_extend_nat : mctt. Lemma exp_eq_sub_sub_compose_cong_nat : forall {Γ Δ Δ' Ψ σ τ σ' τ' M}, {{ Ψ ⊢ M : ℕ }} -> @@ -850,7 +854,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_sub_sub_compose_cong_nat : mcltt. +Hint Resolve exp_eq_sub_sub_compose_cong_nat : mctt. (** *** Other Tedious Lemmas *) @@ -866,9 +870,9 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_eq_weaken_var0_id : mcltt. +Hint Resolve sub_eq_weaken_var0_id : mctt. #[export] -Hint Rewrite -> @sub_eq_weaken_var0_id using mauto 4 : mcltt. +Hint Rewrite -> @sub_eq_weaken_var0_id using mauto 4 : mctt. Lemma exp_eq_sub_sub_compose_cong : forall {Γ Δ Δ' Ψ σ τ σ' τ' M A i}, {{ Ψ ⊢ A : Type@i }} -> @@ -890,7 +894,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_sub_sub_compose_cong : mcltt. +Hint Resolve exp_eq_sub_sub_compose_cong : mctt. Lemma ctxeq_ctx_lookup : forall {Γ Δ A x}, {{ ⊢ Γ ≈ Δ }} -> @@ -906,7 +910,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve ctxeq_ctx_lookup : mcltt. +Hint Resolve ctxeq_ctx_lookup : mctt. Lemma sub_id_on_typ : forall {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> @@ -918,7 +922,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_id_on_typ : mcltt. +Hint Resolve sub_id_on_typ : mctt. Lemma sub_id_extend : forall {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> @@ -930,7 +934,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_id_extend : mcltt. +Hint Resolve sub_id_extend : mctt. Lemma sub_eq_id_on_typ : forall {Γ M M' A i}, {{ Γ ⊢ A : Type@i }} -> @@ -942,7 +946,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_eq_id_on_typ : mcltt. +Hint Resolve sub_eq_id_on_typ : mctt. Lemma sub_eq_id_extend_cong : forall {Γ M M' A i}, {{ Γ ⊢ A : Type@i }} -> @@ -954,7 +958,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_eq_id_extend_cong : mcltt. +Hint Resolve sub_eq_id_extend_cong : mctt. Lemma sub_eq_p_id_extend : forall {Γ M A i}, {{ Γ ⊢ A : Type@i }} -> @@ -966,9 +970,9 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_eq_p_id_extend : mcltt. +Hint Resolve sub_eq_p_id_extend : mctt. #[export] -Hint Rewrite -> @sub_eq_p_id_extend using mauto 4 : mcltt. +Hint Rewrite -> @sub_eq_p_id_extend using mauto 4 : mctt. Lemma sub_q : forall {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> @@ -1006,7 +1010,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_q sub_q_typ sub_q_nat : mcltt. +Hint Resolve sub_q sub_q_typ sub_q_nat : mctt. Lemma exp_eq_var_1_sub_q_sigma_nat : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> @@ -1031,7 +1035,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve exp_eq_var_1_sub_q_sigma_nat : mcltt. +Hint Resolve exp_eq_var_1_sub_q_sigma_nat : mctt. Lemma sub_id_extend_zero : forall {Γ}, {{ ⊢ Γ }} -> @@ -1075,7 +1079,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_id_extend_zero sub_weak_compose_weak_extend_succ_var_1 sub_eq_id_extend_nat_compose_sigma sub_eq_id_extend_compose_sigma : mcltt. +Hint Resolve sub_id_extend_zero sub_weak_compose_weak_extend_succ_var_1 sub_eq_id_extend_nat_compose_sigma sub_eq_id_extend_compose_sigma : mctt. Lemma sub_eq_sigma_compose_weak_id_extend : forall {Γ M A i σ Δ}, {{ Γ ⊢ A : Type@i }} -> @@ -1092,7 +1096,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve sub_eq_sigma_compose_weak_id_extend : mcltt. +Hint Resolve sub_eq_sigma_compose_weak_id_extend : mctt. Lemma sub_eq_q_sigma_id_extend : forall {Γ M A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> @@ -1118,9 +1122,9 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_eq_q_sigma_id_extend : mcltt. +Hint Resolve sub_eq_q_sigma_id_extend : mctt. #[export] -Hint Rewrite -> @sub_eq_q_sigma_id_extend using mauto 4 : mcltt. +Hint Rewrite -> @sub_eq_q_sigma_id_extend using mauto 4 : mctt. Lemma sub_eq_p_q_sigma : forall {Γ A i σ Δ}, {{ Δ ⊢ A : Type@i }} -> @@ -1135,7 +1139,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve sub_eq_p_q_sigma : mcltt. +Hint Resolve sub_eq_p_q_sigma : mctt. Lemma sub_eq_p_q_sigma_nat : forall {Γ σ Δ}, {{ Γ ⊢s σ : Δ }} -> @@ -1146,7 +1150,7 @@ Proof with mautosolve. Qed. #[export] -Hint Resolve sub_eq_p_q_sigma_nat : mcltt. +Hint Resolve sub_eq_p_q_sigma_nat : mctt. Lemma sub_eq_p_p_q_q_sigma_nat : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> @@ -1167,7 +1171,7 @@ Proof with mautosolve 3. Qed. #[export] -Hint Resolve sub_eq_p_p_q_q_sigma_nat : mcltt. +Hint Resolve sub_eq_p_p_q_q_sigma_nat : mctt. Lemma sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : forall {Γ A i σ Δ}, {{ Δ, ℕ ⊢ A : Type@i }} -> @@ -1218,7 +1222,7 @@ Proof with mautosolve 4. Qed. #[export] -Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mcltt. +Hint Resolve sub_eq_q_sigma_compose_weak_weak_extend_succ_var_1 : mctt. (** *** Lemmas for [wf_subtyp] *) @@ -1228,7 +1232,7 @@ Fact wf_subtyp_refl : forall {Γ A i}, Proof. mauto. Qed. #[export] -Hint Resolve wf_subtyp_refl : mcltt. +Hint Resolve wf_subtyp_refl : mctt. Lemma wf_subtyp_ge : forall {Γ i j}, {{ ⊢ Γ }} -> @@ -1239,7 +1243,7 @@ Proof. Qed. #[export] -Hint Resolve wf_subtyp_ge : mcltt. +Hint Resolve wf_subtyp_ge : mctt. Lemma wf_subtyp_sub : forall {Δ A A'}, {{ Δ ⊢ A ⊆ A' }} -> @@ -1257,7 +1261,7 @@ Proof. Qed. #[export] -Hint Resolve wf_subtyp_sub : mcltt. +Hint Resolve wf_subtyp_sub : mctt. Lemma wf_subtyp_univ_weaken : forall {Γ i j A}, {{ Γ ⊢ Type@i ⊆ Type@j }} -> @@ -1286,7 +1290,7 @@ Proof with (do 2 eexists; repeat split; mautosolve). Qed. #[export] -Hint Resolve ctx_sub_ctx_lookup : mcltt. +Hint Resolve ctx_sub_ctx_lookup : mctt. Lemma var_compose_subs : forall {Γ τ Δ σ Ψ i A x}, {{ Ψ ⊢ A : Type@i }} -> @@ -1300,7 +1304,7 @@ Proof. Qed. #[export] -Hint Resolve var_compose_subs : mcltt. +Hint Resolve var_compose_subs : mctt. Lemma sub_lookup_var0 : forall Δ Γ σ M1 M2 B i, {{ Δ ⊢s σ : Γ }} -> @@ -1467,4 +1471,4 @@ Proof. inversion_by_head ctx_lookup. Qed. #[export] -Hint Resolve no_closed_neutral : mcltt. +Hint Resolve no_closed_neutral : mctt. diff --git a/theories/Core/Syntactic/System/Tactics.v b/theories/Core/Syntactic/System/Tactics.v index fa18175..35ade82 100644 --- a/theories/Core/Syntactic/System/Tactics.v +++ b/theories/Core/Syntactic/System/Tactics.v @@ -1,6 +1,6 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic.System Require Export Definitions Lemmas. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic.System Require Export Definitions Lemmas. Import Syntax_Notations. #[global] @@ -14,7 +14,7 @@ Ltac pi_univ_level_tac := end. #[export] -Hint Rewrite -> wf_exp_eq_pi_sub using pi_univ_level_tac : mcltt. +Hint Rewrite -> wf_exp_eq_pi_sub using pi_univ_level_tac : mctt. #[local] Ltac invert_wf_ctx1 H := diff --git a/theories/Core/Syntactic/SystemOpt.v b/theories/Core/Syntactic/SystemOpt.v index 0a430e0..a1a331b 100644 --- a/theories/Core/Syntactic/SystemOpt.v +++ b/theories/Core/Syntactic/SystemOpt.v @@ -1,7 +1,7 @@ From Coq Require Import Setoid. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic Require Export CoreInversions Presup. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic Require Export CoreInversions Presup. Import Syntax_Notations. Add Parametric Morphism i Γ : (wf_exp Γ) @@ -44,9 +44,9 @@ Proof. Qed. #[export] -Hint Resolve wf_subtyp_refl' : mcltt. +Hint Resolve wf_subtyp_refl' : mctt. #[export] -Remove Hints wf_subtyp_refl : mcltt. +Remove Hints wf_subtyp_refl : mctt. Corollary wf_conv' : forall Γ M A i A', {{ Γ ⊢ M : A }} -> @@ -57,9 +57,9 @@ Proof. Qed. #[export] -Hint Resolve wf_conv' : mcltt. +Hint Resolve wf_conv' : mctt. #[export] -Remove Hints wf_conv : mcltt. +Remove Hints wf_conv : mctt. Corollary wf_exp_eq_conv' : forall Γ M M' A A' i, {{ Γ ⊢ M ≈ M' : A }} -> @@ -70,9 +70,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_conv' : mcltt. +Hint Resolve wf_exp_eq_conv' : mctt. #[export] -Remove Hints wf_exp_eq_conv : mcltt. +Remove Hints wf_exp_eq_conv : mctt. Corollary wf_ctx_eq_extend' : forall {Γ Δ A A' i}, {{ ⊢ Γ ≈ Δ }} -> @@ -86,9 +86,9 @@ Proof. Qed. #[export] -Hint Resolve wf_ctx_eq_extend' : mcltt. +Hint Resolve wf_ctx_eq_extend' : mctt. #[export] -Remove Hints wf_ctx_eq_extend : mcltt. +Remove Hints wf_ctx_eq_extend : mctt. Corollary wf_nat' : forall {Γ i}, {{ ⊢ Γ }} -> @@ -100,9 +100,9 @@ Proof. Qed. #[export] -Hint Resolve wf_nat' : mcltt. +Hint Resolve wf_nat' : mctt. #[export] -Remove Hints wf_nat : mcltt. +Remove Hints wf_nat : mctt. Corollary wf_natrec' : forall {Γ A MZ MS M}, {{ Γ ⊢ MZ : A[Id,,zero] }} -> @@ -114,9 +114,9 @@ Proof. Qed. #[export] -Hint Resolve wf_natrec' : mcltt. +Hint Resolve wf_natrec' : mctt. #[export] -Remove Hints wf_natrec : mcltt. +Remove Hints wf_natrec : mctt. Corollary wf_pi_max : forall {Γ A i B j}, {{ Γ ⊢ A : Type@i }} -> @@ -130,7 +130,7 @@ Proof. Qed. #[export] -Hint Resolve wf_pi_max : mcltt. +Hint Resolve wf_pi_max : mctt. Corollary wf_fn' : forall {Γ A M B}, {{ Γ, A ⊢ M : B }} -> @@ -140,9 +140,9 @@ Proof. Qed. #[export] -Hint Resolve wf_fn' : mcltt. +Hint Resolve wf_fn' : mctt. #[export] -Remove Hints wf_fn : mcltt. +Remove Hints wf_fn : mctt. Corollary wf_app' : forall {Γ M N A B}, {{ Γ ⊢ M : Π A B }} -> @@ -156,9 +156,9 @@ Proof. Qed. #[export] -Hint Resolve wf_app' : mcltt. +Hint Resolve wf_app' : mctt. #[export] -Remove Hints wf_app : mcltt. +Remove Hints wf_app : mctt. Lemma wf_exp_eq_typ_sub' : forall Γ σ Δ i j, {{ Γ ⊢s σ : Δ }} -> @@ -167,10 +167,10 @@ Lemma wf_exp_eq_typ_sub' : forall Γ σ Δ i j, Proof. mauto 3. Qed. #[export] -Hint Resolve wf_exp_eq_typ_sub' : mcltt. +Hint Resolve wf_exp_eq_typ_sub' : mctt. #[export] -Hint Rewrite -> wf_exp_eq_typ_sub' using solve [lia | mauto 3] : mcltt. +Hint Rewrite -> wf_exp_eq_typ_sub' using solve [lia | mauto 3] : mctt. Corollary wf_exp_eq_nat_sub' : forall Γ σ Δ i, {{ Γ ⊢s σ : Δ }} -> @@ -182,12 +182,12 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_nat_sub' : mcltt. +Hint Resolve wf_exp_eq_nat_sub' : mctt. #[export] -Remove Hints wf_exp_eq_nat_sub : mcltt. +Remove Hints wf_exp_eq_nat_sub : mctt. #[export] -Hint Rewrite -> wf_exp_eq_nat_sub' using mautosolve 3 : mcltt. +Hint Rewrite -> wf_exp_eq_nat_sub' using mautosolve 3 : mctt. Corollary wf_exp_eq_natrec_cong' : forall {Γ A A' i MZ MZ' MS MS' M M'}, {{ Γ, ℕ ⊢ A ≈ A' : Type@i }} -> @@ -200,9 +200,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_natrec_cong' : mcltt. +Hint Resolve wf_exp_eq_natrec_cong' : mctt. #[export] -Remove Hints wf_exp_eq_natrec_cong : mcltt. +Remove Hints wf_exp_eq_natrec_cong : mctt. Corollary wf_exp_eq_natrec_sub' : forall {Γ σ Δ A MZ MS M}, {{ Γ ⊢s σ : Δ }} -> @@ -215,9 +215,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_natrec_sub' : mcltt. +Hint Resolve wf_exp_eq_natrec_sub' : mctt. #[export] -Remove Hints wf_exp_eq_natrec_sub : mcltt. +Remove Hints wf_exp_eq_natrec_sub : mctt. Corollary wf_exp_eq_nat_beta_zero' : forall {Γ A MZ MS}, {{ Γ ⊢ MZ : A[Id,,zero] }} -> @@ -228,9 +228,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_nat_beta_zero' : mcltt. +Hint Resolve wf_exp_eq_nat_beta_zero' : mctt. #[export] -Remove Hints wf_exp_eq_nat_beta_zero : mcltt. +Remove Hints wf_exp_eq_nat_beta_zero : mctt. Corollary wf_exp_eq_nat_beta_succ' : forall {Γ A MZ MS M}, {{ Γ ⊢ MZ : A[Id,,zero] }} -> @@ -242,9 +242,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_nat_beta_succ' : mcltt. +Hint Resolve wf_exp_eq_nat_beta_succ' : mctt. #[export] -Remove Hints wf_exp_eq_nat_beta_succ : mcltt. +Remove Hints wf_exp_eq_nat_beta_succ : mctt. Corollary wf_exp_eq_pi_sub_max : forall {Γ σ Δ A i B j}, {{ Γ ⊢s σ : Δ }} -> @@ -259,7 +259,7 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_pi_sub_max : mcltt. +Hint Resolve wf_exp_eq_pi_sub_max : mctt. Corollary wf_exp_eq_pi_cong' : forall {Γ A A' B B' i}, {{ Γ ⊢ A ≈ A' : Type@i }} -> @@ -270,9 +270,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_pi_cong' : mcltt. +Hint Resolve wf_exp_eq_pi_cong' : mctt. #[export] -Remove Hints wf_exp_eq_pi_cong : mcltt. +Remove Hints wf_exp_eq_pi_cong : mctt. Corollary wf_exp_eq_pi_cong_max : forall {Γ A A' i B B' j}, {{ Γ ⊢ A ≈ A' : Type@i }} -> @@ -286,7 +286,7 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_pi_cong_max : mcltt. +Hint Resolve wf_exp_eq_pi_cong_max : mctt. Corollary wf_exp_eq_fn_cong' : forall {Γ A A' i B M M'}, {{ Γ ⊢ A ≈ A' : Type@i }} -> @@ -297,9 +297,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_fn_cong' : mcltt. +Hint Resolve wf_exp_eq_fn_cong' : mctt. #[export] -Remove Hints wf_exp_eq_fn_cong : mcltt. +Remove Hints wf_exp_eq_fn_cong : mctt. Corollary wf_exp_eq_fn_sub' : forall {Γ σ Δ A M B}, {{ Γ ⊢s σ : Δ }} -> @@ -310,9 +310,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_fn_sub' : mcltt. +Hint Resolve wf_exp_eq_fn_sub' : mctt. #[export] -Remove Hints wf_exp_eq_fn_sub : mcltt. +Remove Hints wf_exp_eq_fn_sub : mctt. Corollary wf_exp_eq_app_cong' : forall {Γ A B M M' N N'}, {{ Γ ⊢ M ≈ M' : Π A B }} -> @@ -326,9 +326,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_app_cong' : mcltt. +Hint Resolve wf_exp_eq_app_cong' : mctt. #[export] -Remove Hints wf_exp_eq_app_cong : mcltt. +Remove Hints wf_exp_eq_app_cong : mctt. Corollary wf_exp_eq_app_sub' : forall {Γ σ Δ A B M N}, {{ Γ ⊢s σ : Δ }} -> @@ -343,9 +343,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_app_sub' : mcltt. +Hint Resolve wf_exp_eq_app_sub' : mctt. #[export] -Remove Hints wf_exp_eq_app_sub : mcltt. +Remove Hints wf_exp_eq_app_sub : mctt. Corollary wf_exp_eq_pi_beta' : forall {Γ A B M N}, {{ Γ, A ⊢ M : B }} -> @@ -360,9 +360,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_pi_beta' : mcltt. +Hint Resolve wf_exp_eq_pi_beta' : mctt. #[export] -Remove Hints wf_exp_eq_pi_beta : mcltt. +Remove Hints wf_exp_eq_pi_beta : mctt. Corollary wf_exp_eq_pi_eta' : forall {Γ A B M}, {{ Γ ⊢ M : Π A B }} -> @@ -375,9 +375,9 @@ Proof. Qed. #[export] -Hint Resolve wf_exp_eq_pi_eta' : mcltt. +Hint Resolve wf_exp_eq_pi_eta' : mctt. #[export] -Remove Hints wf_exp_eq_pi_eta : mcltt. +Remove Hints wf_exp_eq_pi_eta : mctt. Lemma wf_subtyp_pi' : forall Γ A A' B B' i, {{ Γ ⊢ A ≈ A' : Type@i }} -> @@ -392,9 +392,9 @@ Proof. Qed. #[export] -Hint Resolve wf_subtyp_pi' : mcltt. +Hint Resolve wf_subtyp_pi' : mctt. #[export] -Remove Hints wf_subtyp_pi : mcltt. +Remove Hints wf_subtyp_pi : mctt. Lemma wf_exp_eq_refl_sub' : forall Γ Δ σ A M, @@ -407,6 +407,6 @@ Qed. #[export] -Hint Resolve wf_exp_eq_refl_sub' : mcltt. +Hint Resolve wf_exp_eq_refl_sub' : mctt. #[export] -Remove Hints wf_exp_eq_refl_sub : mcltt. +Remove Hints wf_exp_eq_refl_sub : mctt. diff --git a/theories/Entrypoint.v b/theories/Entrypoint.v index 929cca5..1285d22 100644 --- a/theories/Entrypoint.v +++ b/theories/Entrypoint.v @@ -3,11 +3,11 @@ From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlNativeString Ext From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base Completeness Soundness. -From Mcltt.Core.Syntactic Require Import SystemOpt. -From Mcltt.Extraction Require Import NbE TypeCheck. -From Mcltt.Frontend Require Import Elaborator Parser. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base Completeness Soundness. +From Mctt.Core.Syntactic Require Import SystemOpt. +From Mctt.Extraction Require Import NbE TypeCheck. +From Mctt.Frontend Require Import Elaborator Parser. Import MenhirLibParser.Inter. Import Syntax_Notations. diff --git a/theories/Extraction/Evaluation.v b/theories/Extraction/Evaluation.v index 50c04d5..1eaa9bc 100644 --- a/theories/Extraction/Evaluation.v +++ b/theories/Extraction/Evaluation.v @@ -1,8 +1,8 @@ From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Import Evaluation. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Import Evaluation. Import Domain_Notations. Generalizable All Variables. @@ -74,7 +74,7 @@ with eval_sub_order : sub -> env -> Prop := eval_sub_order {{{ σ ∘ τ }}} p ). #[local] -Hint Constructors eval_exp_order eval_natrec_order eval_app_order eval_sub_order : mcltt. +Hint Constructors eval_exp_order eval_natrec_order eval_app_order eval_sub_order : mctt. Lemma eval_exp_order_sound : forall m p a, {{ ⟦ m ⟧ p ↘ a }} -> @@ -96,7 +96,7 @@ Proof with (econstructor; intros; functional_eval_rewrite_clear; eauto). Qed. #[export] -Hint Resolve eval_exp_order_sound eval_natrec_order_sound eval_app_order_sound eval_sub_order_sound : mcltt. +Hint Resolve eval_exp_order_sound eval_natrec_order_sound eval_app_order_sound eval_sub_order_sound : mctt. #[local] Ltac impl_obl_tac1 := diff --git a/theories/Extraction/NbE.v b/theories/Extraction/NbE.v index d8c2aea..bf71ebf 100644 --- a/theories/Extraction/NbE.v +++ b/theories/Extraction/NbE.v @@ -1,9 +1,9 @@ From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Export NbE. -From Mcltt.Extraction Require Import Evaluation Readback. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Export NbE. +From Mctt.Extraction Require Import Evaluation Readback. Import Domain_Notations. Generalizable All Variables. @@ -17,7 +17,7 @@ Inductive initial_env_order : ctx -> Prop := initial_env_order (A :: Γ)). #[local] -Hint Constructors initial_env_order : mcltt. +Hint Constructors initial_env_order : mctt. Lemma initial_env_order_sound : forall Γ p, initial_env Γ p -> @@ -27,7 +27,7 @@ Proof with (econstructor; intros; functional_initial_env_rewrite_clear; function Qed. #[local] -Hint Resolve initial_env_order_sound : mcltt. +Hint Resolve initial_env_order_sound : mctt. Section InitialEnvImpl. @@ -101,7 +101,7 @@ Inductive nbe_order G M A : Prop := nbe_order G M A ). #[local] -Hint Constructors nbe_order : mcltt. +Hint Constructors nbe_order : mctt. Lemma nbe_order_sound : forall G M A w, nbe G M A w -> @@ -115,7 +115,7 @@ Proof with (econstructor; intros; Qed. #[local] -Hint Resolve nbe_order_sound : mcltt. +Hint Resolve nbe_order_sound : mctt. Section NbEDef. @@ -159,7 +159,7 @@ Inductive nbe_ty_order G A : Prop := nbe_ty_order G A ). #[local] -Hint Constructors nbe_ty_order : mcltt. +Hint Constructors nbe_ty_order : mctt. Lemma nbe_ty_order_sound : forall G A w, nbe_ty G A w -> @@ -173,7 +173,7 @@ Proof with (econstructor; intros; Qed. #[local] -Hint Resolve nbe_ty_order_sound : mcltt. +Hint Resolve nbe_ty_order_sound : mctt. Section NbETyDef. diff --git a/theories/Extraction/PseudoMonadic.v b/theories/Extraction/PseudoMonadic.v index 7abb526..99fc2ca 100644 --- a/theories/Extraction/PseudoMonadic.v +++ b/theories/Extraction/PseudoMonadic.v @@ -1,3 +1,4 @@ +(** McTT Extraction Helpers in a (pseudo-)monadic style *) From Coq Require Extraction. (** We cannot use class based generalization for diff --git a/theories/Extraction/Readback.v b/theories/Extraction/Readback.v index 4eb8b53..3f569cb 100644 --- a/theories/Extraction/Readback.v +++ b/theories/Extraction/Readback.v @@ -1,9 +1,9 @@ From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Import Readback Evaluation. -From Mcltt.Extraction Require Import Evaluation. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Import Readback Evaluation. +From Mctt.Extraction Require Import Evaluation. Import Domain_Notations. Generalizable All Variables. @@ -78,7 +78,7 @@ with read_typ_order : nat -> domain -> Prop := read_typ_order s d{{{ ⇑ a b }}} ). #[local] -Hint Constructors read_nf_order read_ne_order read_typ_order : mcltt. +Hint Constructors read_nf_order read_ne_order read_typ_order : mctt. Lemma read_nf_order_sound : forall s d m, {{ Rnf d in s ↘ m }} -> @@ -96,7 +96,7 @@ Proof with (econstructor; intros; functional_eval_rewrite_clear; mauto). Qed. #[export] -Hint Resolve read_nf_order_sound read_ne_order_sound read_typ_order_sound : mcltt. +Hint Resolve read_nf_order_sound read_ne_order_sound read_typ_order_sound : mctt. #[local] Ltac impl_obl_tac1 := diff --git a/theories/Extraction/Subtyping.v b/theories/Extraction/Subtyping.v index c1e84d9..03629c4 100644 --- a/theories/Extraction/Subtyping.v +++ b/theories/Extraction/Subtyping.v @@ -1,7 +1,7 @@ -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Algorithmic Require Export Subtyping. -From Mcltt.Extraction Require Import NbE PseudoMonadic. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Algorithmic Require Export Subtyping. +From Mctt.Extraction Require Import NbE PseudoMonadic. From Equations Require Import Equations. Import Domain_Notations. @@ -54,7 +54,7 @@ Inductive subtyping_order G A B := nbe_ty_order G B -> subtyping_order G A B. #[local] -Hint Constructors subtyping_order : mcltt. +Hint Constructors subtyping_order : mctt. Lemma subtyping_order_sound : forall G A B, {{ G ⊢a A ⊆ B }} -> @@ -101,7 +101,7 @@ Proof. Qed. #[local] -Hint Resolve subtyping_order_sound subtyping_impl_complete' : mcltt. +Hint Resolve subtyping_order_sound subtyping_impl_complete' : mctt. Theorem subtyping_impl_complete : forall G A B, {{G ⊢a A ⊆ B}} -> diff --git a/theories/Extraction/TypeCheck.v b/theories/Extraction/TypeCheck.v index 53c20d2..bd29572 100644 --- a/theories/Extraction/TypeCheck.v +++ b/theories/Extraction/TypeCheck.v @@ -1,12 +1,12 @@ From Coq Require Import Morphisms_Relations. From Equations Require Import Equations. -From Mcltt Require Import LibTactics. -From Mcltt.Algorithmic Require Import Typing. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Semantic Require Import Consequences Realizability. -From Mcltt.Extraction Require Import NbE PseudoMonadic Subtyping. -From Mcltt.Frontend Require Import Elaborator. +From Mctt Require Import LibTactics. +From Mctt.Algorithmic Require Import Typing. +From Mctt.Core Require Import Base. +From Mctt.Core.Semantic Require Import Consequences Realizability. +From Mctt.Extraction Require Import NbE PseudoMonadic Subtyping. +From Mctt.Frontend Require Import Elaborator. Import Domain_Notations. Section lookup. @@ -68,7 +68,7 @@ Section type_check. . #[local] - Hint Constructors type_check_order type_infer_order : mcltt. + Hint Constructors type_check_order type_infer_order : mctt. Lemma user_exp_to_type_infer_order : forall M, user_exp M -> @@ -348,7 +348,7 @@ Section type_check. End type_check. #[local] -Hint Resolve type_check_order_soundness type_infer_order_soundness : mcltt. +Hint Resolve type_check_order_soundness type_infer_order_soundness : mctt. Lemma type_check_complete' : forall G M A (HA : exists i, {{ G ⊢ A : Type@i }}), {{ G ⊢a M ⟸ A }} -> diff --git a/theories/Frontend/Elaborator.v b/theories/Frontend/Elaborator.v index ba7d0b1..b83e46c 100644 --- a/theories/Frontend/Elaborator.v +++ b/theories/Frontend/Elaborator.v @@ -1,8 +1,8 @@ From Coq Require Import Lia List MSets PeanoNat String FunInd. -From Mcltt Require Import LibTactics. -From Mcltt.Core Require Import Base. -From Mcltt.Core.Syntactic Require Import Syntax. +From Mctt Require Import LibTactics. +From Mctt.Core Require Import Base. +From Mctt.Core.Syntactic Require Import Syntax. Open Scope string_scope. @@ -104,7 +104,7 @@ Inductive user_exp : exp -> Prop := `( user_exp (a_var x) ). #[export] -Hint Constructors user_exp : mcltt. +Hint Constructors user_exp : mctt. Lemma user_exp_nf : forall M, user_exp (nf_to_exp M) with user_exp_ne : forall M, user_exp (ne_to_exp M). @@ -151,7 +151,7 @@ Inductive closed_at : exp -> nat -> Prop := | ca_natrec : forall n m z s l, closed_at n l -> closed_at m (1+l) -> closed_at z l -> closed_at s (2+l) -> closed_at (a_natrec m z s n) l . #[local] -Hint Constructors closed_at: mcltt. +Hint Constructors closed_at: mctt. (** Lemma for the well_scoped proof, lookup succeeds if var is in context *) Lemma lookup_known (s : string) (ctx : list string) (H_in : List.In s ctx) : exists n : nat, (lookup s ctx = Some n /\ n < List.length ctx). diff --git a/theories/Frontend/Parser.vy b/theories/Frontend/Parser.vy index 6980e1a..c39d83a 100644 --- a/theories/Frontend/Parser.vy +++ b/theories/Frontend/Parser.vy @@ -2,7 +2,7 @@ From Coq Require Import List Arith.PeanoNat String. -From Mcltt Require Import Syntax. +From Mctt Require Import Syntax. Parameter loc : Type. diff --git a/theories/LibTactics.v b/theories/LibTactics.v index f59546a..8236038 100644 --- a/theories/LibTactics.v +++ b/theories/LibTactics.v @@ -3,7 +3,7 @@ From Equations Require Export Equations. Open Scope predicate_scope. -Create HintDb mcltt discriminated. +Create HintDb mctt discriminated. (** Transparency setting for generalized rewriting *) #[export] @@ -191,37 +191,37 @@ Ltac dir_inversion_clear_by_head head := match_by_head head ltac:(fun H => direc Ltac destruct_by_head head := match_by_head head ltac:(fun H => destruct H). Ltac dir_destruct_by_head head := match_by_head head ltac:(fun H => directed destruct H). -(** *** McLTT automation *) +(** *** McTT automation *) Tactic Notation "mauto" := - eauto with mcltt core. + eauto with mctt core. Tactic Notation "mauto" int_or_var(pow) := - eauto pow with mcltt core. + eauto pow with mctt core. Tactic Notation "mauto" "using" uconstr(use) := - eauto using use with mcltt core. + eauto using use with mctt core. Tactic Notation "mauto" "using" uconstr(use1) "," uconstr(use2) := - eauto using use1, use2 with mcltt core. + eauto using use1, use2 with mctt core. Tactic Notation "mauto" "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) := - eauto using use1, use2, use3 with mcltt core. + eauto using use1, use2, use3 with mctt core. Tactic Notation "mauto" "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) "," uconstr(use4) := - eauto using use1, use2, use3, use4 with mcltt core. + eauto using use1, use2, use3, use4 with mctt core. Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use) := - eauto pow using use with mcltt core. + eauto pow using use with mctt core. Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2) := - eauto pow using use1, use2 with mcltt core. + eauto pow using use1, use2 with mctt core. Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) := - eauto pow using use1, use2, use3 with mcltt core. + eauto pow using use1, use2, use3 with mctt core. Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) "," uconstr(use4) := - eauto pow using use1, use2, use3, use4 with mcltt core. + eauto pow using use1, use2, use3, use4 with mctt core. Ltac mautosolve_impl pow := unshelve solve [mauto pow]; solve [constructor]. @@ -244,7 +244,7 @@ Hint Extern 1 (@Transitive _ (@predicate_implication _)) => simple apply @PreOrd (** Default setting for [intuition] tactic *) -Ltac Tauto.intuition_solver ::= auto with mcltt core solve_subterm. +Ltac Tauto.intuition_solver ::= auto with mctt core solve_subterm. Ltac exvar T tac := lazymatch type of T with @@ -464,7 +464,7 @@ Qed. Ltac bulky_rewrite1 := match goal with | H : _ |- _ => rewrite H - | _ => progress (autorewrite with mcltt) + | _ => progress (autorewrite with mctt) end. Ltac bulky_rewrite := repeat (bulky_rewrite1; mauto 2). @@ -472,7 +472,7 @@ Ltac bulky_rewrite := repeat (bulky_rewrite1; mauto 2). Ltac bulky_rewrite_in1 HT := match goal with | H : _ |- _ => tryif unify H HT then fail else rewrite H in HT - | _ => progress (autorewrite with mcltt in HT) + | _ => progress (autorewrite with mctt in HT) end. Ltac bulky_rewrite_in HT := repeat (bulky_rewrite_in1 HT; mauto 2). diff --git a/theories/Makefile b/theories/Makefile index 52eb44e..09ef36f 100644 --- a/theories/Makefile +++ b/theories/Makefile @@ -44,7 +44,7 @@ clean: $(COQMAKEFILE) .PHONY: update_CoqProject update_CoqProject: clean - (echo "-R . Mcltt"; \ + (echo "-R . Mctt"; \ echo ""; \ echo "-arg -w -arg -cast-in-pattern,-notation-overridden"; \ echo ""; \ diff --git a/theories/_CoqProject b/theories/_CoqProject index f1d7c4a..3b90e99 100644 --- a/theories/_CoqProject +++ b/theories/_CoqProject @@ -1,4 +1,4 @@ --R . Mcltt +-R . Mctt -arg -w -arg -cast-in-pattern,-notation-overridden