From 110d0976d741057cc0225a1d89f24182245049ec Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Wed, 22 Oct 2025 20:06:46 +0200 Subject: [PATCH 01/21] Updated project config --- FormArith.opam | 3 +- Makefile | 999 +++++++++++++++++++++++++++++++++++++++++++++++++ README.md | 6 +- _CoqProject | 4 +- 4 files changed, 1007 insertions(+), 5 deletions(-) create mode 100644 Makefile diff --git a/FormArith.opam b/FormArith.opam index 53f83c5..9ccff1e 100644 --- a/FormArith.opam +++ b/FormArith.opam @@ -5,8 +5,9 @@ authors: "FormArith contributors" homepage: "https://github.com/bwerner/FormArith" bug-reports: "https://github.com/bwerner/FormArith/issues" depends: [ - "coq" { (= "8.17.1" ) } + "coq" { (= "8.19.2" ) } "dune" {>= "3.8"} + "coq-autosubst" {>= "1.9"} ] build: ["dune" "build" "-p" name "-j" jobs] install: ["dune" "install" "-p" name] diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..cfe38b1 --- /dev/null +++ b/Makefile @@ -0,0 +1,999 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # Copyright INRIA, CNRS and contributors ## +## /dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=command time +endif +endif +else +STDTIME?=command time -f $(TIMEFMT) +endif + +COQBIN?= +ifneq (,$(COQBIN)) +# add an ending / +COQBIN:=$(COQBIN)/ +endif + +# Coq binaries +COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" +COQCHK ?= "$(COQBIN)coqchk" +COQNATIVE ?= "$(COQBIN)coqnative" +COQDEP ?= "$(COQBIN)coqdep" +COQDOC ?= "$(COQBIN)coqdoc" +COQPP ?= "$(COQBIN)coqpp" +COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" + +# Timing scripts +COQMAKE_ONE_TIME_FILE ?= "$(COQCORELIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQCORELIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQCORELIB)/tools/make-both-single-timing-files.py" +BEFORE ?= +AFTER ?= + +# OCaml binaries +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkall +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkall +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack + +# DESTDIR is prepended to all installation paths +DESTDIR ?= + +# Debug builds, typically -g to OCaml, -debug to Coq. +CAMLDEBUG ?= +COQDEBUG ?= + +# Extra packages to be linked in (as in findlib -package) +CAMLPKGS ?= +FINDLIBPKGS = -package coq-core.plugins.ltac $(CAMLPKGS) + +# Option for making timing files +TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= +# Option for including the memory column(s) +TIMING_INCLUDE_MEM?= +# Option for sorting by the memory column +TIMING_SORT_BY_MEM?= +# Output file names for timed builds +TIME_OF_BUILD_FILE ?= time-of-build.log +TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log +TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log +TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log +TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log +TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line + +TGTS ?= + +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) +endif + +# Substitution of the path by appending $(DESTDIR) if needed. +# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. +windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) +destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) + +# Installation paths of libraries and documentation. +COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) +COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/coq/user-contrib) +COQPLUGININSTALL ?= $(call destination_path,$(COQCORELIB)/..) +COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? + +# findlib files installation +FINDLIBPREINST= mkdir -p "$(COQPLUGININSTALL)/" +FINDLIBDESTDIR= -destdir "$(COQPLUGININSTALL)/" + +# we need to move out of sight $(METAFILE) otherwise findlib thinks the +# package is already installed +findlib_install = \ + $(HIDE)if [ "$(METAFILE)" ]; then \ + $(FINDLIBPREINST) && \ + mv "$(METAFILE)" "$(METAFILE).skip" ; \ + "$(OCAMLFIND)" install $(2) $(FINDLIBDESTDIR) $(FINDLIBPACKAGE) $(1); \ + rc=$$?; \ + mv "$(METAFILE).skip" "$(METAFILE)"; \ + exit $$rc; \ + fi +findlib_remove = \ + $(HIDE)if [ ! -z "$(METAFILE)" ]; then\ + "$(OCAMLFIND)" remove $(FINDLIBDESTDIR) $(FINDLIBPACKAGE); \ + fi + + +########## End of parameters ################################################## +# What follows may be relevant to you only if you need to +# extend this Makefile. If so, look for 'Extension point' here and +# put in Makefile.local double colon rules accordingly. +# E.g. to perform some work after the all target completes you can write +# +# post-all:: +# echo "All done!" +# +# in Makefile.local +# +############################################################################### + + + + +# Flags ####################################################################### +# +# We define a bunch of variables combining the parameters. +# To add additional flags to coq, coqchk or coqdoc, set the +# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. +# To overwrite the default choice and set your own flags entirely, set the +# {COQ,COQCHK,COQDOC}FLAGS variable. + +SHOW := $(if $(VERBOSE),@true "",@echo "") +HIDE := $(if $(VERBOSE),,@) + +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) + +OPT?= + +# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d +ifeq '$(OPT)' '-byte' +USEBYTE:=true +DYNOBJ:=.cma +DYNLIB:=.cma +else +USEBYTE:= +DYNOBJ:=.cmxs +DYNLIB:=.cmxs +endif + +# these variables are meant to be overridden if you want to add *extra* flags +COQEXTRAFLAGS?= +COQCHKEXTRAFLAGS?= +COQDOCEXTRAFLAGS?= + +# Find the last argument of the form "-native-compiler FLAG" +COQUSERNATIVEFLAG:=$(strip \ +$(subst -native-compiler-,,\ +$(lastword \ +$(filter -native-compiler-%,\ +$(subst -native-compiler ,-native-compiler-,\ +$(strip $(COQEXTRAFLAGS))))))) + +COQFILTEREDEXTRAFLAGS:=$(strip \ +$(filter-out -native-compiler-%,\ +$(subst -native-compiler ,-native-compiler-,\ +$(strip $(COQEXTRAFLAGS))))) + +COQACTUALNATIVEFLAG:=$(lastword $(COQMF_COQ_NATIVE_COMPILER_DEFAULT) $(COQMF_COQPROJECTNATIVEFLAG) $(COQUSERNATIVEFLAG)) + +ifeq '$(COQACTUALNATIVEFLAG)' 'yes' + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" + COQDONATIVE="yes" +else +ifeq '$(COQACTUALNATIVEFLAG)' 'ondemand' + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" + COQDONATIVE="no" +else + COQNATIVEFLAG="-w" "-deprecated-native-compiler-option" "-native-compiler" "no" + COQDONATIVE="no" +endif +endif + +# these flags do NOT contain the libraries, to make them easier to overwrite +COQFLAGS?=-q $(OTHERFLAGS) $(COQFILTEREDEXTRAFLAGS) $(COQNATIVEFLAG) +COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) +COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) + +COQDOCLIBS?=$(COQLIBS_NOML) + +# The version of Coq being run and the version of coq_makefile that +# generated this makefile +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) +COQMAKEFILE_VERSION:=8.19.2 + +# COQ_SRC_SUBDIRS is for user-overriding, usually to add +# `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for +# Coq's own core libraries, which should be replaced by ocamlfind +# options at some point. +COQ_SRC_SUBDIRS?= +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") + +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) + +ifneq (,$(TIMING)) + ifeq (after,$(TIMING)) + TIMING_EXT=after-timing + else + ifeq (before,$(TIMING)) + TIMING_EXT=before-timing + else + TIMING_EXT=timing + endif + endif + TIMING_ARG=-time-file $<.$(TIMING_EXT) +else + TIMING_ARG= +endif + +ifneq (,$(PROFILING)) + PROFILE_ARG=-profile $<.prof.json + PROFILE_ZIP=gzip $<.prof.json +else + PROFILE_ARG= + PROFILE_ZIP=true +endif + +# Files ####################################################################### +# +# We here define a bunch of variables about the files being part of the +# Coq project in order to ease the writing of build target and build rules + +VDFILE := .Makefile.d + +ALLSRCFILES := \ + $(MLGFILES) \ + $(MLFILES) \ + $(MLPACKFILES) \ + $(MLLIBFILES) \ + $(MLIFILES) + +# helpers +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) +strip_dotslash = $(patsubst ./%,%,$(1)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + +VO = vo +VOS = vos + +VOFILES = $(VFILES:.v=.$(VO)) +GLOBFILES = $(VFILES:.v=.glob) +HTMLFILES = $(VFILES:.v=.html) +GHTMLFILES = $(VFILES:.v=.g.html) +BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) +TEXFILES = $(VFILES:.v=.tex) +GTEXFILES = $(VFILES:.v=.g.tex) +CMOFILES = \ + $(MLGFILES:.mlg=.cmo) \ + $(MLFILES:.ml=.cmo) \ + $(MLPACKFILES:.mlpack=.cmo) +CMXFILES = $(CMOFILES:.cmo=.cmx) +OFILES = $(CMXFILES:.cmx=.o) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) +CMXAFILES = $(CMAFILES:.cma=.cmxa) +CMIFILES = \ + $(CMOFILES:.cmo=.cmi) \ + $(MLIFILES:.mli=.cmi) +# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just +# a .mlg file +CMXSFILES = \ + $(MLPACKFILES:.mlpack=.cmxs) \ + $(CMXAFILES:.cmxa=.cmxs) \ + $(if $(MLPACKFILES)$(CMXAFILES),,\ + $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) + +# files that are packed into a plugin (no extension) +PACKEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) +# files that are archived into a .cma (mllib) +LIBEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) +CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) +CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) +OBJFILES = $(call vo_to_obj,$(VOFILES)) +ALLNATIVEFILES = \ + $(OBJFILES:.o=.cmi) \ + $(OBJFILES:.o=.cmx) \ + $(OBJFILES:.o=.cmxs) +FINDLIBPACKAGE=$(patsubst .%,%,$(suffix $(METAFILE))) + +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) +FILESTOINSTALL = \ + $(VOFILES) \ + $(VFILES) \ + $(GLOBFILES) \ + $(NATIVEFILES) \ + $(CMXSFILES) # to be removed when we remove legacy loading +FINDLIBFILESTOINSTALL = \ + $(CMIFILESTOINSTALL) +ifeq '$(HASNATDYNLINK)' 'true' +DO_NATDYNLINK = yes +FINDLIBFILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) +else +DO_NATDYNLINK = +endif + +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) + +# Compilation targets ######################################################### + +all: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all + +all.timing.diff: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all.timing.diff + +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + +ifeq (0,$(TIMING_INCLUDE_MEM)) +TIMING_INCLUDE_MEM_ARG := --no-include-mem +else +TIMING_INCLUDE_MEM_ARG := +endif + +ifeq (1,$(TIMING_SORT_BY_MEM)) +TIMING_SORT_BY_MEM_ARG := --sort-by-mem +else +TIMING_SORT_BY_MEM_ARG := +endif + +make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) +make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) +make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) + $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed +print-pretty-timed:: + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +print-pretty-timed-diff:: + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +ifeq (,$(BEFORE)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +endif +endif +pretty-timed: + $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff + +# Extension points for actions to be performed before/after the all target +pre-all:: + @# Extension point + $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ + echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ + echo "W: while the current Coq version is $(COQ_VERSION)";\ + fi +.PHONY: pre-all + +post-all:: + @# Extension point +.PHONY: post-all + +real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) +.PHONY: real-all + +real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) +.PHONY: real-all.timing.diff + +bytefiles: $(CMOFILES) $(CMAFILES) +.PHONY: bytefiles + +optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) +.PHONY: optfiles + +# FIXME, see Ralf's bugreport +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") +.PHONY: quick + +vio2vo: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ + -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +.PHONY: vio2vo + +# quick2vo is undocumented +quick2vo: + $(HIDE)make -j $(J) vio + $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ + viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ + if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ + done); \ + echo "VIO2VO: $$VIOFILES"; \ + if [ -n "$$VIOFILES" ]; then \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ + fi +.PHONY: quick2vo + +checkproofs: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ + -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) +.PHONY: checkproofs + +vos: $(VOFILES:%.vo=%.vos) +.PHONY: vos + +vok: $(VOFILES:%.vo=%.vok) +.PHONY: vok + +validate: $(VOFILES) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ +.PHONY: validate + +only: $(TGTS) +.PHONY: only + +# Documentation targets ####################################################### + +html: $(GLOBFILES) $(VFILES) + $(SHOW)'COQDOC -d html $(GAL)' + $(HIDE)mkdir -p html + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) + +mlihtml: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -d $@' + $(HIDE)mkdir $@ || rm -rf $@/* + $(HIDE)$(CAMLDOC) -html \ + -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) + +all-mli.tex: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) $(FINDLIBPKGS) + +all.ps: $(VFILES) + $(SHOW)'COQDOC -ps $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(VFILES)` + +all.pdf: $(VFILES) + $(SHOW)'COQDOC -pdf $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(VFILES)` + +# FIXME: not quite right, since the output name is different +gallinahtml: GAL=-g +gallinahtml: html + +all-gal.ps: GAL=-g +all-gal.ps: all.ps + +all-gal.pdf: GAL=-g +all-gal.pdf: all.pdf + +# ? +beautify: $(BEAUTYFILES) + for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done + @echo 'Do not do "make clean" until you are sure that everything went well!' + @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' +.PHONY: beautify + +# Installation targets ######################################################## +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. + +# We use $(file) to avoid generating a very long command string to pass to the shell +# (cf https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Strange.20command.20length.20limit.20on.20Linux) +# However Apple ships old make which doesn't have $(file) so we need a fallback +$(file >.hasfile,1) +HASFILE:=$(shell if [ -e .hasfile ]; then echo 1; rm .hasfile; fi) + +MKFILESTOINSTALL= $(if $(HASFILE),$(file >.filestoinstall,$(FILESTOINSTALL)),\ + $(shell rm -f .filestoinstall) \ + $(foreach x,$(FILESTOINSTALL),$(shell printf '%s\n' "$x" >> .filestoinstall))) + +# findlib needs the package to not be installed, so we remove it before +# installing it (see the call to findlib_remove) +install: META + @$(MKFILESTOINSTALL) + $(HIDE)code=0; for f in $$(cat .filestoinstall); do\ + if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ + done; exit $$code + $(HIDE)for f in $$(cat .filestoinstall); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ + done + $(call findlib_remove) + $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) + $(HIDE)$(MAKE) install-extra -f "$(SELF)" + @rm -f .filestoinstall +install-extra:: + @# Extension point +.PHONY: install install-extra + +META: $(METAFILE) + $(HIDE)if [ "$(METAFILE)" ]; then \ + cat "$(METAFILE)" | grep -v 'directory.*=.*' > META; \ + fi + +install-byte: + $(call findlib_install, $(CMAFILES) $(CMOFILESTOINSTALL), -add) + +install-doc:: html mlihtml + @# Extension point + $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)for i in html/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done + $(HIDE)install -d \ + "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE)for i in mlihtml/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done +.PHONY: install-doc + +uninstall:: + @# Extension point + @$(MKFILESTOINSTALL) + $(call findlib_remove) + $(HIDE)for f in $$(cat .filestoinstall); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" ;\ + done + $(HIDE)for f in $$(cat .filestoinstall); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + echo RMDIR "$(COQLIBINSTALL)/$$df/" &&\ + (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ + done + @rm -f .filestoinstall + +.PHONY: uninstall + +uninstall-doc:: + @# Extension point + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true +.PHONY: uninstall-doc + +# Cleaning #################################################################### +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. + +clean:: + @# Extension point + $(SHOW)'CLEAN' + $(HIDE)rm -f $(CMOFILES) + $(HIDE)rm -f $(CMIFILES) + $(HIDE)rm -f $(CMAFILES) + $(HIDE)rm -f $(CMXFILES) + $(HIDE)rm -f $(CMXAFILES) + $(HIDE)rm -f $(CMXSFILES) + $(HIDE)rm -f $(OFILES) + $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(MLGFILES:.mlg=.ml) + $(HIDE)rm -f $(CMXFILES:.cmx=.cmt) + $(HIDE)rm -f $(MLIFILES:.mli=.cmti) + $(HIDE)rm -f $(ALLDFILES) + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)find . -name .coq-native -type d -empty -delete + $(HIDE)rm -f $(VOFILES) + $(HIDE)rm -f $(VOFILES:.vo=.vio) + $(HIDE)rm -f $(VOFILES:.vo=.vos) + $(HIDE)rm -f $(VOFILES:.vo=.vok) + $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) + $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex + $(HIDE)rm -f $(VFILES:.v=.glob) + $(HIDE)rm -f $(VFILES:.v=.tex) + $(HIDE)rm -f $(VFILES:.v=.g.tex) + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)rm -f META + $(HIDE)rm -rf html mlihtml +.PHONY: clean + +cleanall:: clean + @# Extension point + $(SHOW)'CLEAN *.aux *.timing' + $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) + $(HIDE)rm -f .lia.cache .nia.cache +.PHONY: cleanall + +archclean:: + @# Extension point + $(SHOW)'CLEAN *.cmx *.o' + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) +.PHONY: archclean + + +# Compilation rules ########################################################### + +$(MLIFILES:.mli=.cmi): %.cmi: %.mli + $(SHOW)'CAMLC -c $<' + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< + +$(MLGFILES:.mlg=.ml): %.ml: %.mlg + $(SHOW)'COQPP $<' + $(HIDE)$(COQPP) $< + +# Stupid hack around a deficient syntax: we cannot concatenate two expansions +$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml + $(SHOW)'CAMLC -c $<' + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $< + +# Same hack +$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml + $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' + $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) $(FOR_PACK) $< + + +$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -o $@ $< + +$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + +$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + + +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx | %.mlpack + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< + +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack + $(SHOW)'CAMLC -pack -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack + $(SHOW)'CAMLOPT -pack -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -pack -o $@ $^ + +# This rule is for _CoqProject with no .mllib nor .mlpack +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx + $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) \ + -shared -o $@ $< + +# can't make +# https://www.gnu.org/software/make/manual/make.html#Static-Pattern +# work with multiple target rules +# so use eval in a loop instead +# with grouped targets https://www.gnu.org/software/make/manual/make.html#Multiple-Targets +# if available (GNU Make >= 4.3) +ifneq (,$(filter grouped-target,$(.FEATURES))) +define globvorule= + +# take care to $$ variables using $< etc + $(1).vo $(1).glob &: $(1).v | $$(VDFILE) + $$(SHOW)COQC $(1).v + $$(HIDE)$$(TIMER) $$(COQC) $$(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $$(COQFLAGS) $$(COQLIBS) $(1).v + $$(HIDE)$$(PROFILE_ZIP) +ifeq ($(COQDONATIVE), "yes") + $$(SHOW)COQNATIVE $(1).vo + $$(HIDE)$$(call TIMER,$(1).vo.native) $$(COQNATIVE) $$(COQLIBS) $(1).vo +endif + +endef +else + +$(VOFILES): %.vo: %.v | $(VDFILE) + $(SHOW)COQC $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $< + $(HIDE)$(PROFILE_ZIP) +ifeq ($(COQDONATIVE), "yes") + $(SHOW)COQNATIVE $@ + $(HIDE)$(call TIMER,$@.native) $(COQNATIVE) $(COQLIBS) $@ +endif + +# this is broken :( todo fix if we ever find a solution that doesn't need grouped targets +$(GLOBFILES): %.glob: %.v + $(SHOW)'COQC $< (for .glob)' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +endif + +$(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile)))) + +$(VFILES:.v=.vio): %.vio: %.v + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vos): %.vos: %.v + $(SHOW)COQC -vos $< + $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vok): %.vok: %.v + $(SHOW)COQC -vok $< + $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing + $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + +$(BEAUTYFILES): %.v.beautified: %.v + $(SHOW)'BEAUTIFY $<' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< + +$(TEXFILES): %.tex: %.v + $(SHOW)'COQDOC -latex $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ + +$(GTEXFILES): %.g.tex: %.v + $(SHOW)'COQDOC -latex -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ + +$(HTMLFILES): %.html: %.v %.glob + $(SHOW)'COQDOC -html $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ + +$(GHTMLFILES): %.g.html: %.v %.glob + $(SHOW)'COQDOC -html -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + +# Dependency files ############################################################ + +ifndef MAKECMDGOALS + -include $(ALLDFILES) +else + ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) + endif +endif + +.SECONDARY: $(ALLDFILES) + +redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) + +GENMLFILES:=$(MLGFILES:.mlg=.ml) +$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) + +$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) + +# If this makefile is created using a _CoqProject we have coqdep get +# options from it. This avoids argument length limits for pathological +# projects. Note that extra options might be on the command line. +VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) + +$(VDFILE): _CoqProject $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) $(if $(strip $(METAFILE)),-m "$(METAFILE)") -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) + +# Misc ######################################################################## + +byte: + $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" +.PHONY: byte + +opt: + $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" +.PHONY: opt + +# This is deprecated. To extend this makefile use +# extension points and Makefile.local +printenv:: + $(warning printenv is deprecated) + $(warning write extensions in Makefile.local or include Makefile.conf) + @echo 'COQLIB = $(COQLIB)' + @echo 'COQCORELIB = $(COQCORELIB)' + @echo 'DOCDIR = $(DOCDIR)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' + @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' + @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' + @echo 'COQCORE_SRC_SUBDIRS = $(COQCORE_SRC_SUBDIRS)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'PP = $(PP)' + @echo 'COQFLAGS = $(COQFLAGS)' + @echo 'COQLIB = $(COQLIBS)' + @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' + @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' +.PHONY: printenv + +# Generate a .merlin file. If you need to append directives to this +# file you can extend the merlin-hook target in Makefile.local +.merlin: + $(SHOW)'FILL .merlin' + $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin + $(HIDE)echo 'B $(COQCORELIB)' >> .merlin + $(HIDE)echo 'S $(COQCORELIB)' >> .merlin + $(HIDE)$(foreach d,$(COQCORE_SRC_SUBDIRS), \ + echo 'B $(COQCORELIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo 'S $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) + $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" +.PHONY: merlin + +merlin-hook:: + @# Extension point +.PHONY: merlin-hook + +# prints all variables +debug: + $(foreach v,\ + $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ + $(.VARIABLES))),\ + $(info $(v) = $($(v)))) +.PHONY: debug + +.DEFAULT_GOAL := all + +# Users can create Makefile.local-late to hook into double-colon rules +# or add other needed Makefile code, using defined +# variables if necessary. +-include Makefile.local-late + +# Local Variables: +# mode: makefile-gmake +# End: diff --git a/README.md b/README.md index c0a4c3e..21b6059 100644 --- a/README.md +++ b/README.md @@ -42,20 +42,20 @@ We assume that you have `opam` installed on your system. Setup instructions can 1. Create a new `opam` switch for this project: ```bash -opam switch create --packages=ocaml-variants.4.14.2+options,ocaml-option-flambda +opam switch create 4.14.2 opam switch ``` 2. Install the necessary dependencies: ```bash -opam pin add coq 8.19.2 opam repo add coq-released https://coq.inria.fr/opam/released +opam install . --deps-only ``` 3. Build the Rocq implementation: ```bash -dune build +make ``` diff --git a/_CoqProject b/_CoqProject index d86752a..059d15c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1 +1,3 @@ --Q _build/default/theories/ FormArith +-Q theories FormArith + +theories \ No newline at end of file From c52c466dd1f0f4bd52ae567431862942f2ebe125 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Wed, 22 Oct 2025 21:07:46 +0200 Subject: [PATCH 02/21] Basic definitions of terms, substitutions and convesion for the lambda cube --- theories/LambdaCube/Term.v | 109 +++++++++++++++++++++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 theories/LambdaCube/Term.v diff --git a/theories/LambdaCube/Term.v b/theories/LambdaCube/Term.v new file mode 100644 index 0000000..145ed36 --- /dev/null +++ b/theories/LambdaCube/Term.v @@ -0,0 +1,109 @@ +From Coq Require Import Utf8. +From Coq Require Import Arith Lia. + +Inductive sort : Type := +| Star : sort +| Box : sort. + +Inductive term (n : nat) : Type := +| Var : {k | k < n} → term n +| Pi : term n → term (S n) → term n +| Abs : term n → term (S n) → term n +| App : term n → term n → term n +| Srt : sort → term n +. + +Arguments Var {n}. +Arguments Pi {n}. +Arguments Abs {n}. +Arguments App {n}. +Arguments Srt {n}. + +Definition weaken {k : nat} (i : {i | i < k}) : {i | i < S k} := + exist _ (proj1_sig i) (Nat.lt_lt_succ_r _ _ (proj2_sig i)). + +Definition lift + {k n : nat} (σ : {i | i < k} → {i | i < n}) + (i : {i | i < S k}) : {i | i < S n} + := + match lt_dec (proj1_sig i) k with + | left Hi => weaken (σ (exist _ (proj1_sig i) Hi)) + | right _ => exist _ n (Nat.lt_succ_diag_r n) + end. + +Lemma sig_lt_ext {k : nat} (p q : {i | i < k}) : + proj1_sig p = proj1_sig q → p = q. +Proof. + destruct p, q. + simpl. + intros ->. + f_equal. + apply le_unique. +Qed. + +Lemma lift_lt {k n : nat} (σ : {i | i < k} → {i | i < n}) (i : nat) + : ∀ Hik HiSk, proj1_sig (lift σ (exist _ i HiSk)) = proj1_sig (σ (exist _ i Hik)). +Proof. + intros Hik HiSk. + simpl. + unfold lift. + destruct (lt_dec _ _); [|now contradict Hik]. + simpl. + do 2 f_equal. + now apply sig_lt_ext. +Qed. + +Lemma lift_eq {k n : nat} (σ : {i | i < k} → {i | i < n}) + : ∀ Hk, proj1_sig (lift σ (exist _ k Hk)) = n. +Proof. + intros. + unfold lift. + destruct (lt_dec _ _); simpl in *; [lia|reflexivity]. +Qed. + +Fixpoint subst {k n : nat} (σ : {i | i < k} → {i | i < n}) (t : term k) : term n := + match t with + | Var i => Var (σ i) + | Pi ty fam => Pi (subst σ ty) (subst (lift σ) fam) + | Abs ty tm => Abs (subst σ ty) (subst (lift σ) tm) + | App tm1 tm2 => App (subst σ tm1) (subst σ tm2) + | Srt s => Srt s + end. + +Definition lift_bind {k n : nat} (σ : {i | i < k} → term n) (i : {i | i < S k}) : term (S n) := + match lt_dec (proj1_sig i) k with + | left Hi => subst weaken (σ (exist _ (proj1_sig i) Hi)) + | right _ => Var (exist _ n (Nat.lt_succ_diag_r n)) + end. + +Fixpoint bind {k n : nat} (σ : {i | i < k} → term n) (t : term k) : term n + := + match t with + | Var i => σ i + | Pi ty fam => Pi (bind σ ty) (bind (lift_bind σ) fam) + | Abs ty tm => Abs (bind σ ty) (bind (lift_bind σ) tm) + | App tm1 tm2 => App (bind σ tm1) (bind σ tm2) + | Srt s => Srt s + end. + +Definition bind_first {k : nat} (t : term k) (i : {i | i < S k}) : term k + := + match lt_dec (proj1_sig i) k with + | left Hi => Var (exist _ (proj1_sig i) Hi) + | right _ => t + end. + +Inductive conv {n : nat} : term n → term n → Prop := +| conv_var (k : {k | k < n}) : conv (Var k) (Var k) +| conv_srt (s : sort) : conv (Srt s) (Srt s) +| conv_pi (A1 A2 : term n) (B1 B2 : term (S n)) : + conv A1 A2 → conv B1 B2 → conv (Pi A1 B1) (Pi A2 B2) +| conv_abs (A1 A2 : term n) (B1 B2 : term (S n)) : + conv A1 A2 → conv B1 B2 → conv (Abs A1 B1) (Abs A2 B2) +| conv_app (A1 A2 B1 B2 : term n) : + conv A1 A2 → conv B1 B2 → conv (App A1 B1) (App A2 B2) +| conv_redex_l (A1 A2 A3 : term n) (B : term (S n)) : + conv (bind (bind_first A2) B) A3 → conv (App (Abs A1 B) A2) A3 +| conv_redex_r (A1 A2 A3 : term n) (B : term (S n)) : + conv A3 (bind (bind_first A2) B) → conv A3 (App (Abs A1 B) A2) +. From ce14f56dc2da60c6acfd1b7a13fea4e462cb6606 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Thu, 23 Oct 2025 14:29:52 +0200 Subject: [PATCH 03/21] Added notion of contexts for the lambda cube --- theories/Base.v | 7 + theories/LambdaCube/Operational.v | 13 ++ theories/LambdaCube/Term.v | 296 +++++++++++++++++++++++++++--- 3 files changed, 286 insertions(+), 30 deletions(-) create mode 100644 theories/LambdaCube/Operational.v diff --git a/theories/Base.v b/theories/Base.v index bc56e61..60170c8 100644 --- a/theories/Base.v +++ b/theories/Base.v @@ -5,6 +5,7 @@ Require Export Nat. Require Export Relations.Relations. +From Coq Require Export Utf8. (** Force all the proof to have only one goal at a time. *) #[export] Set Default Goal Selector "!". @@ -13,6 +14,12 @@ Require Export Relations.Relations. Notation "R *" := (clos_refl_trans _ R) (at level 8, no associativity, format "R *"). +(** Composition of functions **) + +Notation "g ∘ f" := + (fun x => g (f x)) + (at level 40, left associativity). + Tactic Notation "inv" hyp(H) := inversion H; subst; clear H. diff --git a/theories/LambdaCube/Operational.v b/theories/LambdaCube/Operational.v new file mode 100644 index 0000000..143727f --- /dev/null +++ b/theories/LambdaCube/Operational.v @@ -0,0 +1,13 @@ +From Coq Require Import Utf8. +From FormArith Require Import Base. +From FormArith.LambdaCube Require Import Term. + +Inductive head_step {n : nat} : term n → term n → Prop := +| beta_red + (ty : term n) + (body : term (S n)) + (arg : term n) : head_step (App (Abs ty body) arg) (bind (bind_first arg) body). + +Inductive step {n : nat} : term n → term n → Prop := +| ctx_red (K : ctx n) (t u : term n) : + head_step t u → step (fill K t) (fill K u). diff --git a/theories/LambdaCube/Term.v b/theories/LambdaCube/Term.v index 145ed36..dfabeca 100644 --- a/theories/LambdaCube/Term.v +++ b/theories/LambdaCube/Term.v @@ -1,5 +1,6 @@ From Coq Require Import Utf8. From Coq Require Import Arith Lia. +From FormArith Require Import Base. Inductive sort : Type := | Star : sort @@ -10,8 +11,7 @@ Inductive term (n : nat) : Type := | Pi : term n → term (S n) → term n | Abs : term n → term (S n) → term n | App : term n → term n → term n -| Srt : sort → term n -. +| Srt : sort → term n. Arguments Var {n}. Arguments Pi {n}. @@ -19,6 +19,33 @@ Arguments Abs {n}. Arguments App {n}. Arguments Srt {n}. +Inductive ctx (n : nat) : Type := +| Hole : ctx n +| PiL : ctx n → term (S n) → ctx n +| AbsL : ctx n → term (S n) → ctx n +| AppL : ctx n → term n → ctx n +| PiR : term n → ctx (S n) → ctx n +| AbsR : term n → ctx (S n) → ctx n +| AppR : term n → ctx n → ctx n. + +Arguments Hole {n}. +Arguments PiL {n}. +Arguments AbsL {n}. +Arguments AppL {n}. +Arguments PiR {n}. +Arguments AbsR {n}. +Arguments AppR {n}. + +Lemma sig_lt_ext {k : nat} (p q : {i | i < k}) : + proj1_sig p = proj1_sig q → p = q. +Proof. + destruct p, q. + simpl. + intros ->. + f_equal. + apply le_unique. +Qed. + Definition weaken {k : nat} (i : {i | i < k}) : {i | i < S k} := exist _ (proj1_sig i) (Nat.lt_lt_succ_r _ _ (proj2_sig i)). @@ -31,14 +58,51 @@ Definition lift | right _ => exist _ n (Nat.lt_succ_diag_r n) end. -Lemma sig_lt_ext {k : nat} (p q : {i | i < k}) : - proj1_sig p = proj1_sig q → p = q. +Lemma lift_weaken + {k n : nat} + (σ : {i | i < k} → {i | i < n}) + (i : {i | i < k}) : + lift σ (weaken i) = weaken (σ i). Proof. - destruct p, q. - simpl. - intros ->. - f_equal. - apply le_unique. + unfold lift. + destruct (lt_dec _ _) as [|Hge]. + - do 2 f_equal. + now apply sig_lt_ext. + - contradict Hge. + simpl. + apply proj2_sig. +Qed. + +Lemma lift_ext + {k n : nat} + (σ1 σ2: {i | i < k} → {i | i < n}) : + (∀ i, σ1 i = σ2 i) → + ∀ (i : {i | i < S k}), + lift σ1 i = lift σ2 i. +Proof. + intros σ_eq i. + unfold lift. + destruct (lt_dec (proj1_sig i) k). + - congruence. + - reflexivity. +Qed. + +Lemma lift_comp : + ∀ {k m n : nat} + (σ1 : {i | i < k} → {i | i < m}) + (σ2 : {i | i < m} → {i | i < n}) + (i : {i | i < S k}), + lift σ2 (lift σ1 i) = lift (σ2 ∘ σ1) i. +Proof. + intros k m n σ1 σ2 i. + unfold lift. + destruct (lt_dec (proj1_sig i) k); + destruct (lt_dec _ _) as [Hlt | Hge]; simpl in *; try lia. + - do 2 f_equal. + now apply sig_lt_ext. + - contradict Hge. + apply proj2_sig. + - reflexivity. Qed. Lemma lift_lt {k n : nat} (σ : {i | i < k} → {i | i < n}) (i : nat) @@ -61,21 +125,129 @@ Proof. destruct (lt_dec _ _); simpl in *; [lia|reflexivity]. Qed. -Fixpoint subst {k n : nat} (σ : {i | i < k} → {i | i < n}) (t : term k) : term n := +(* Renaming of free variables in a term *) +Fixpoint ren {k n : nat} (σ : {i | i < k} → {i | i < n}) (t : term k) : term n := match t with | Var i => Var (σ i) - | Pi ty fam => Pi (subst σ ty) (subst (lift σ) fam) - | Abs ty tm => Abs (subst σ ty) (subst (lift σ) tm) - | App tm1 tm2 => App (subst σ tm1) (subst σ tm2) + | Pi ty fam => Pi (ren σ ty) (ren (lift σ) fam) + | Abs ty tm => Abs (ren σ ty) (ren (lift σ) tm) + | App tm1 tm2 => App (ren σ tm1) (ren σ tm2) | Srt s => Srt s end. +(* Renaming of free variables in a context *) +Fixpoint renK {k n : nat} (σ : {i | i < k} → {i | i < n}) (K : ctx k) : ctx n := + match K with + | Hole => Hole + | PiL K fam => PiL (renK σ K) (ren (lift σ) fam) + | AbsL K tm => AbsL (renK σ K) (ren (lift σ) tm) + | AppL K tm2 => AppL (renK σ K) (ren σ tm2) + | PiR ty K => PiR (ren σ ty) (renK (lift σ) K) + | AbsR ty K => AbsR (ren σ ty) (renK (lift σ) K) + | AppR tm1 K => AppR (ren σ tm1) (renK σ K) + end. + +Fixpoint fill {n : nat} (K : ctx n) (t : term n) : term n := + match K with + | Hole => t + | PiL K fam => Pi (fill K t) fam + | AbsL K tm => Abs (fill K t) tm + | AppL K tm => App (fill K t) tm + | PiR ty K => Pi ty (fill K (ren weaken t)) + | AbsR ty K => Abs ty (fill K (ren weaken t)) + | AppR tm K => App tm (fill K t) + end. + +Lemma ren_ext : + ∀ {k n : nat} + (σ1 σ2: {i | i < k} → {i | i < n}) + (t : term k), + (∀ i, σ1 i = σ2 i) → + ren σ1 t = ren σ2 t. +Proof. + fix IH 5. + intros k n σ1 σ2 t σ_eq. + destruct t; + simpl; + try congruence; + f_equal; + try now apply IH. + all : apply IH, lift_ext, σ_eq. +Qed. + +Lemma ren_comp : + ∀ {k m n : nat} + (σ1 : {i | i < k} → {i | i < m}) + (σ2 : {i | i < m} → {i | i < n}) + (t : term k), + ren σ2 (ren σ1 t) = ren (σ2 ∘ σ1) t. +Proof. + fix IH 6. + intros k m n σ1 σ2 t. + destruct t; simpl; try easy. + 1,2 : + rewrite !IH; + f_equal; + apply ren_ext; + intros i; + apply lift_comp. + now rewrite !IH. +Qed. + +Lemma ren_fill : + ∀ {k n : nat} + (σ : {i | i < k} → {i | i < n}) + (K : ctx k) (t : term k), + ren σ (fill K t) = fill (renK σ K) (ren σ t). +Proof. + fix IH 4. + intros k n σ K t. + destruct K; simpl; try congruence. + all: + f_equal; + rewrite IH; + f_equal; + rewrite !ren_comp; + apply ren_ext; + intros i; + apply lift_weaken. +Qed. + Definition lift_bind {k n : nat} (σ : {i | i < k} → term n) (i : {i | i < S k}) : term (S n) := match lt_dec (proj1_sig i) k with - | left Hi => subst weaken (σ (exist _ (proj1_sig i) Hi)) + | left Hi => ren weaken (σ (exist _ (proj1_sig i) Hi)) | right _ => Var (exist _ n (Nat.lt_succ_diag_r n)) end. - + +Lemma lift_bind_weaken + {k n : nat} + (σ : {i | i < k} → term n) + (i : {i | i < k}) : + lift_bind σ (weaken i) = ren weaken (σ i). +Proof. + unfold lift_bind. + destruct (lt_dec _ _) as [|Hge]. + - do 2 f_equal. + now apply sig_lt_ext. + - contradict Hge. + simpl. + apply proj2_sig. +Qed. + +Lemma lift_bind_ext + {k n : nat} + (σ1 σ2: {i | i < k} → term n) : + (∀ i, σ1 i = σ2 i) → + ∀ (i : {i | i < S k}), + lift_bind σ1 i = lift_bind σ2 i. +Proof. + intros σ_eq i. + unfold lift_bind. + destruct (lt_dec (proj1_sig i) k). + - congruence. + - reflexivity. +Qed. + Fixpoint bind {k n : nat} (σ : {i | i < k} → term n) (t : term k) : term n := match t with @@ -86,24 +258,88 @@ Fixpoint bind {k n : nat} (σ : {i | i < k} → term n) (t : term k) : term n | Srt s => Srt s end. +Fixpoint bindK {k n : nat} (σ : {i | i < k} → term n) (K : ctx k) : ctx n := + match K with + | Hole => Hole + | PiL K fam => PiL (bindK σ K) (bind (lift_bind σ) fam) + | AbsL K tm => AbsL (bindK σ K) (bind (lift_bind σ) tm) + | AppL K tm2 => AppL (bindK σ K) (bind σ tm2) + | PiR ty K => PiR (bind σ ty) (bindK (lift_bind σ) K) + | AbsR ty K => AbsR (bind σ ty) (bindK (lift_bind σ) K) + | AppR tm1 K => AppR (bind σ tm1) (bindK σ K) + end. + +Lemma lift_bind_comp : + ∀ {k m n : nat} + (σ1 : {i | i < k} → term m) + (σ2 : {i | i < m} → term n) + (i : {i | i < S k}), + bind (lift_bind σ2) (lift_bind σ1 i) = lift_bind (bind σ2 ∘ σ1) i. +Proof. +Abort. + + + +Lemma bind_ext : + ∀ {k n : nat} + (σ1 σ2: {i | i < k} → term n) + (t : term k), + (∀ i, σ1 i = σ2 i) → + bind σ1 t = bind σ2 t. +Proof. + fix IH 5. + intros k n σ1 σ2 t σ_eq. + destruct t; + simpl; + try congruence; + f_equal; + try now apply IH. + all : apply IH, lift_bind_ext, σ_eq. +Qed. + +Lemma bind_comp : + ∀ {k m n : nat} + (σ1 : {i | i < k} → term m) + (σ2 : {i | i < m} → term n) + (t : term k), + bind σ2 (bind σ1 t) = bind (bind σ2 ∘ σ1) t. +Proof. + fix IH 6. + intros k m n σ1 σ2 t. + destruct t; simpl; try reflexivity. + 1,2 : + rewrite !IH; + f_equal; + apply bind_ext; + intros i. + apply lift_comp. + now rewrite !IH. +Qed. + +Lemma ren_fill : + ∀ {k n : nat} + (σ : {i | i < k} → {i | i < n}) + (K : ctx k) (t : term k), + ren σ (fill K t) = fill (renK σ K) (ren σ t). +Proof. + fix IH 4. + intros k n σ K t. + destruct K; simpl; try congruence. + all: + f_equal; + rewrite IH; + f_equal; + rewrite !ren_comp; + apply ren_ext; + intros i; + apply lift_weaken. +Qed. + + + Definition bind_first {k : nat} (t : term k) (i : {i | i < S k}) : term k := match lt_dec (proj1_sig i) k with | left Hi => Var (exist _ (proj1_sig i) Hi) | right _ => t end. - -Inductive conv {n : nat} : term n → term n → Prop := -| conv_var (k : {k | k < n}) : conv (Var k) (Var k) -| conv_srt (s : sort) : conv (Srt s) (Srt s) -| conv_pi (A1 A2 : term n) (B1 B2 : term (S n)) : - conv A1 A2 → conv B1 B2 → conv (Pi A1 B1) (Pi A2 B2) -| conv_abs (A1 A2 : term n) (B1 B2 : term (S n)) : - conv A1 A2 → conv B1 B2 → conv (Abs A1 B1) (Abs A2 B2) -| conv_app (A1 A2 B1 B2 : term n) : - conv A1 A2 → conv B1 B2 → conv (App A1 B1) (App A2 B2) -| conv_redex_l (A1 A2 A3 : term n) (B : term (S n)) : - conv (bind (bind_first A2) B) A3 → conv (App (Abs A1 B) A2) A3 -| conv_redex_r (A1 A2 A3 : term n) (B : term (S n)) : - conv A3 (bind (bind_first A2) B) → conv A3 (App (Abs A1 B) A2) -. From f245bb454396b4533b2f4a4ab6024d1dbd779227 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Thu, 23 Oct 2025 14:36:20 +0200 Subject: [PATCH 04/21] Aborted unfinished lemmas in LambdaCube/Term.v --- theories/LambdaCube/Term.v | 25 +++++-------------------- 1 file changed, 5 insertions(+), 20 deletions(-) diff --git a/theories/LambdaCube/Term.v b/theories/LambdaCube/Term.v index dfabeca..990933d 100644 --- a/theories/LambdaCube/Term.v +++ b/theories/LambdaCube/Term.v @@ -312,31 +312,16 @@ Proof. f_equal; apply bind_ext; intros i. - apply lift_comp. - now rewrite !IH. -Qed. +Abort. -Lemma ren_fill : +Lemma bind_fill : ∀ {k n : nat} - (σ : {i | i < k} → {i | i < n}) + (σ : {i | i < k} → term n) (K : ctx k) (t : term k), - ren σ (fill K t) = fill (renK σ K) (ren σ t). + bind σ (fill K t) = fill (bindK σ K) (bind σ t). Proof. - fix IH 4. - intros k n σ K t. - destruct K; simpl; try congruence. - all: - f_equal; - rewrite IH; - f_equal; - rewrite !ren_comp; - apply ren_ext; - intros i; - apply lift_weaken. -Qed. +Abort. - - Definition bind_first {k : nat} (t : term k) (i : {i | i < S k}) : term k := match lt_dec (proj1_sig i) k with From 5485d01d739ef102fe4bd5cd166bff8350dc3f3d Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Thu, 23 Oct 2025 14:38:04 +0200 Subject: [PATCH 05/21] added Makefile.conf to gitignore --- .gitignore | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.gitignore b/.gitignore index 8296c73..c5ef405 100644 --- a/.gitignore +++ b/.gitignore @@ -47,6 +47,8 @@ time-of-build-before.log time-of-build-both.log time-of-build-pretty.log +# Makefile gitignore +Makefile.conf # == Dune gitignore From 133f1b3dfc479f36b231bad1428db747b9784fbd Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Thu, 23 Oct 2025 14:45:47 +0200 Subject: [PATCH 06/21] Minor comments --- theories/LambdaCube/Term.v | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/theories/LambdaCube/Term.v b/theories/LambdaCube/Term.v index 990933d..c4b8b15 100644 --- a/theories/LambdaCube/Term.v +++ b/theories/LambdaCube/Term.v @@ -6,6 +6,11 @@ Inductive sort : Type := | Star : sort | Box : sort. +(* Terms of the Lambda Cube with n free variables. + Variables are represented as De Bruijn levels. + The free variable most recently introduced in + a term with (n + 1) free variables has value n + *) Inductive term (n : nat) : Type := | Var : {k | k < n} → term n | Pi : term n → term (S n) → term n @@ -19,6 +24,7 @@ Arguments Abs {n}. Arguments App {n}. Arguments Srt {n}. +(* Execution contexts of the Lambda Cube with n free variables. *) Inductive ctx (n : nat) : Type := | Hole : ctx n | PiL : ctx n → term (S n) → ctx n @@ -46,9 +52,11 @@ Proof. apply le_unique. Qed. +(* Basic weakening renaming *) Definition weaken {k : nat} (i : {i | i < k}) : {i | i < S k} := exist _ (proj1_sig i) (Nat.lt_lt_succ_r _ _ (proj2_sig i)). +(* Lifting of variable renamings *) Definition lift {k n : nat} (σ : {i | i < k} → {i | i < n}) (i : {i | i < S k}) : {i | i < S n} @@ -147,6 +155,7 @@ Fixpoint renK {k n : nat} (σ : {i | i < k} → {i | i < n}) (K : ctx k) : ctx n | AppR tm1 K => AppR (ren σ tm1) (renK σ K) end. +(* Plug a term in place of the hole in a context *) Fixpoint fill {n : nat} (K : ctx n) (t : term n) : term n := match K with | Hole => t @@ -212,7 +221,8 @@ Proof. intros i; apply lift_weaken. Qed. - + +(* Lifting of variable substitutions *) Definition lift_bind {k n : nat} (σ : {i | i < k} → term n) (i : {i | i < S k}) : term (S n) := match lt_dec (proj1_sig i) k with | left Hi => ren weaken (σ (exist _ (proj1_sig i) Hi)) @@ -248,6 +258,7 @@ Proof. - reflexivity. Qed. +(* Substitution of free variables inside a term *) Fixpoint bind {k n : nat} (σ : {i | i < k} → term n) (t : term k) : term n := match t with @@ -258,6 +269,7 @@ Fixpoint bind {k n : nat} (σ : {i | i < k} → term n) (t : term k) : term n | Srt s => Srt s end. +(* Substitution of free variables inside a context *) Fixpoint bindK {k n : nat} (σ : {i | i < k} → term n) (K : ctx k) : ctx n := match K with | Hole => Hole @@ -278,8 +290,6 @@ Lemma lift_bind_comp : Proof. Abort. - - Lemma bind_ext : ∀ {k n : nat} (σ1 σ2: {i | i < k} → term n) @@ -321,7 +331,8 @@ Lemma bind_fill : bind σ (fill K t) = fill (bindK σ K) (bind σ t). Proof. Abort. - + +(* Basic substitution capturing the free variable introduced last *) Definition bind_first {k : nat} (t : term k) (i : {i | i < S k}) : term k := match lt_dec (proj1_sig i) k with From a61f4c911edf1cc9e0250231bedad992d4393625 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Fri, 14 Nov 2025 14:52:43 +0100 Subject: [PATCH 07/21] Proved most lemmas needed for subtitutions --- theories/LambdaCube/Term.v | 152 ++++++++++++++++++++++++++++++++++--- 1 file changed, 141 insertions(+), 11 deletions(-) diff --git a/theories/LambdaCube/Term.v b/theories/LambdaCube/Term.v index c4b8b15..640a884 100644 --- a/theories/LambdaCube/Term.v +++ b/theories/LambdaCube/Term.v @@ -281,15 +281,6 @@ Fixpoint bindK {k n : nat} (σ : {i | i < k} → term n) (K : ctx k) : ctx n := | AppR tm1 K => AppR (bind σ tm1) (bindK σ K) end. -Lemma lift_bind_comp : - ∀ {k m n : nat} - (σ1 : {i | i < k} → term m) - (σ2 : {i | i < m} → term n) - (i : {i | i < S k}), - bind (lift_bind σ2) (lift_bind σ1 i) = lift_bind (bind σ2 ∘ σ1) i. -Proof. -Abort. - Lemma bind_ext : ∀ {k n : nat} (σ1 σ2: {i | i < k} → term n) @@ -307,6 +298,143 @@ Proof. all : apply IH, lift_bind_ext, σ_eq. Qed. +Lemma lift_bind_lift : + ∀ {k m n : nat} + (σ1 : {i | i < k} → {i | i < m}) + (σ2 : {i | i < m} → term n) + (i : {i | i < S k}), + lift_bind σ2 (lift σ1 i) = lift_bind (σ2 ∘ σ1) i. +Proof. + intros k m n σ1 σ2 i. + unfold lift at 1, lift_bind at 2. + destruct (lt_dec _ _). + - unfold lift_bind at 1. + destruct (lt_dec _ _) as [|Hge]. + + do 2 f_equal. + now apply sig_lt_ext. + + contradict Hge. + simpl. + apply proj2_sig. + - unfold lift_bind at 1. + destruct (lt_dec _ _) as [Hlt|]. + + simpl in Hlt. lia. + + reflexivity. +Qed. + +Lemma bind_ren : + ∀ {k m n : nat} + (σ1 : {i | i < k} → {i | i < m}) + (σ2 : {i | i < m} → term n) + (t : term k), + bind σ2 (ren σ1 t) = bind (σ2 ∘ σ1) t. +Proof. + fix IH 6. + intros k m n σ1 σ2 t. + destruct t; simpl; try reflexivity. + 1,2: + rewrite IH; + f_equal; + rewrite IH; + apply bind_ext; + intros i; + apply lift_bind_lift. + now rewrite !IH. +Qed. + +Lemma lift_bind_ren : + ∀ {k m n : nat} + (σ1 : {i | i < k} → term m) + (σ2 : {i | i < m} → {i | i < n}) + (i : {i : nat | i < S k}), + ren (lift σ2) (lift_bind σ1 i) = + lift_bind (ren σ2 ∘ σ1) i. +Proof. + intros k m n σ1 σ2 i. + unfold lift_bind. + destruct (lt_dec _ _) as [|Hge]. + + rewrite !ren_comp. + apply ren_ext, lift_weaken. + + simpl. f_equal. + apply sig_lt_ext. + simpl. + apply lift_eq. +Qed. + +Lemma ren_bind : + ∀ {k m n : nat} + (σ1 : {i | i < k} → term m) + (σ2 : {i | i < m} → {i | i < n}) + (t : term k), + ren σ2 (bind σ1 t) = bind (ren σ2 ∘ σ1) t. +Proof. + fix IH 6. + intros k m n σ1 σ2 t. + destruct t; simpl; try reflexivity. + - rewrite IH. + f_equal. + rewrite IH. + apply bind_ext. + intros i. + apply lift_bind_ren. + - rewrite !IH. + f_equal. + apply bind_ext. + intros i. + apply lift_bind_ren. + - now rewrite !IH. +Qed. + +Lemma bind_weaken : + ∀ {k n : nat} + (σ : {i | i < k} → term n) + (t : term k), + bind (lift_bind σ) (ren weaken t) = ren weaken (bind σ t). +Proof. + fix IH 4. + intros k n σ t. + destruct t; simpl. + - apply lift_bind_weaken. + - rewrite IH. + f_equal. + rewrite ren_bind, bind_ren. + apply bind_ext. + intros i. + rewrite lift_bind_ren, lift_bind_lift. + apply lift_bind_ext. + intros j. + apply lift_bind_weaken. + - rewrite IH. + f_equal. + rewrite ren_bind, bind_ren. + apply bind_ext. + intros i. + rewrite lift_bind_ren, lift_bind_lift. + apply lift_bind_ext. + intros j. + apply lift_bind_weaken. + - now rewrite !IH. + - reflexivity. +Qed. + +Lemma lift_bind_comp : + ∀ {k m n : nat} + (σ1 : {i | i < k} → term m) + (σ2 : {i | i < m} → term n) + (i : {i | i < S k}), + bind (lift_bind σ2) (lift_bind σ1 i) = lift_bind (bind σ2 ∘ σ1) i. +Proof. + intros k m n σ1 σ2 i. + unfold lift_bind at 2 3. + destruct (lt_dec _ _) as [Hge | Hlt]. + - rewrite ren_bind, bind_ren. + apply bind_ext. + apply lift_bind_weaken. + - simpl. + unfold lift_bind. + destruct (lt_dec _ _) as [Hge | Hlt']; [simpl in Hge; lia|]. + reflexivity. +Qed. + Lemma bind_comp : ∀ {k m n : nat} (σ1 : {i | i < k} → term m) @@ -321,8 +449,10 @@ Proof. rewrite !IH; f_equal; apply bind_ext; - intros i. -Abort. + intros i; + apply lift_bind_comp. + now rewrite !IH. +Qed. Lemma bind_fill : ∀ {k n : nat} From e4ca361c1c7bad752626f674090ea5d50330fed8 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Fri, 14 Nov 2025 15:02:27 +0100 Subject: [PATCH 08/21] Proved lemma about interaction of substitution and fill --- theories/LambdaCube/Term.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/theories/LambdaCube/Term.v b/theories/LambdaCube/Term.v index 640a884..06d4558 100644 --- a/theories/LambdaCube/Term.v +++ b/theories/LambdaCube/Term.v @@ -460,7 +460,16 @@ Lemma bind_fill : (K : ctx k) (t : term k), bind σ (fill K t) = fill (bindK σ K) (bind σ t). Proof. -Abort. + fix IH 4. + intros k n σ K t. + destruct K; simpl; try congruence. + all: rewrite IH; + do 2 f_equal; + rewrite bind_ren, + ren_bind; + apply bind_ext; + apply lift_bind_weaken. +Qed. (* Basic substitution capturing the free variable introduced last *) Definition bind_first {k : nat} (t : term k) (i : {i | i < S k}) : term k From 6b51b2661f749691d223e6ad117c77d5a07f6a00 Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Sun, 16 Nov 2025 04:56:52 +0100 Subject: [PATCH 09/21] proved confluence of beta-reduction (after rectifying the definition of beta-reduction --- theories/LambdaCube/Operational.v | 244 +++++++++++++++++++++++++++++- theories/LambdaCube/Term.v | 137 +++++++---------- 2 files changed, 299 insertions(+), 82 deletions(-) diff --git a/theories/LambdaCube/Operational.v b/theories/LambdaCube/Operational.v index 143727f..58fbd58 100644 --- a/theories/LambdaCube/Operational.v +++ b/theories/LambdaCube/Operational.v @@ -1,13 +1,251 @@ From Coq Require Import Utf8. +From Coq Require Import Arith Lia. From FormArith Require Import Base. From FormArith.LambdaCube Require Import Term. +Reserved Notation "t [≻] u" (at level 70). +Reserved Notation "t ≻ u" (at level 70). +Reserved Notation "t ≻+ u" (at level 70). +Reserved Notation "t ≻* u" (at level 70). +Reserved Notation "t ≅ u" (at level 70). + Inductive head_step {n : nat} : term n → term n → Prop := | beta_red (ty : term n) (body : term (S n)) - (arg : term n) : head_step (App (Abs ty body) arg) (bind (bind_first arg) body). + (arg : term n) : App (Abs ty body) arg [≻] bind (bind_first arg) body +where "t [≻] u" := (head_step t u). Inductive step {n : nat} : term n → term n → Prop := -| ctx_red (K : ctx n) (t u : term n) : - head_step t u → step (fill K t) (fill K u). +| ctx_red {k} (K : ctx n k) (t u : term k) : + t [≻] u → fill K t ≻ fill K u +where "t ≻ u" := (step t u). + +Lemma step_under_context {n k} (K: ctx n k) t u : t ≻ u -> fill K t ≻ fill K u. +Proof. + destruct 1 as [K']. do 2 rewrite <- fill_fillK. constructor. assumption. +Qed. + +Inductive Rplus {A} (R: relation A) a b : Prop := +| add_last_R m : Rplus R a m -> R m b -> Rplus R a b +| Rclot_plus : R a b -> Rplus R a b. + +Notation "t ≻+ u" := (Rplus step t u). + +Lemma Rplus_trans {A} (R: relation A) x y z : Rplus R x y -> Rplus R y z -> Rplus R x z. +Proof. + induction 2. + - econstructor; eauto. + - econstructor; eauto. +Qed. + +Lemma add_first {A} (R: relation A) x y z : R x y -> Rplus R y z -> Rplus R x z. + induction 2. + - econstructor; eauto. + - econstructor; eauto. constructor. auto. +Qed. + +Inductive Rstar {A} (R: relation A) a : A -> Prop := +| Rstar_refl : Rstar R a a +| Rclot_plus_star b : Rplus R a b -> Rstar R a b. + +Notation "t ≻* u" := (Rstar step t u). + +Lemma step_star_context {n k} (K: ctx n k) t u : t ≻* u -> fill K t ≻* fill K u. +Proof. + destruct 1; constructor. induction H. + - econstructor; try eassumption. apply step_under_context. assumption. + - constructor. apply step_under_context. assumption. +Qed. + +Lemma Rstar_trans {A} (R: relation A) x y z : Rstar R x y -> Rstar R y z -> Rstar R x z. +Proof. + destruct 1; auto. + destruct 1. + - constructor. assumption. + - constructor. eapply Rplus_trans; eassumption. +Qed. + +Inductive Requiv {A} (R: relation A) a : A -> Prop := +| Rclot_plus_equiv b : Rplus R a b -> Requiv R a b +| Rclot_plus_equiv_r b : Rplus R b a -> Requiv R a b +| Requiv_refl : Requiv R a a. + +Reserved Notation "t ⪼ u" (at level 70). +Reserved Notation "t ⪼+ u" (at level 70). +Reserved Notation "t ⪼* u" (at level 70). + +Inductive par_step {n: nat} : term n -> term n -> Prop := +| par_step_var i : Var i ⪼ Var i +| par_step_sort s : Srt s ⪼ Srt s +| par_step_pi t1 t2 u1 u2 : t1 ⪼ u1 -> t2 ⪼ u2 -> Pi t1 t2 ⪼ Pi u1 u2 +| par_step_abs t1 t2 u1 u2 : t1 ⪼ u1 -> t2 ⪼ u2 -> Abs t1 t2 ⪼ Abs u1 u2 +| par_step_app t1 t2 u1 u2 : t1 ⪼ u1 -> t2 ⪼ u2 -> App t1 t2 ⪼ App u1 u2 +| par_step_redex T f arg f' arg' : + f ⪼ f' -> arg ⪼ arg' -> App (Abs T f) arg ⪼ bind (bind_first arg') f' +where "t ⪼ u" := (par_step t u). + +Notation "t ⪼+ u" := (Rplus par_step t u). +Notation "t ⪼* u" := (Rstar par_step t u). + +Lemma par_refl {n} (t : term n) : t ⪼ t. +Proof. + induction t; constructor; assumption. +Qed. + +Fixpoint par_max {n} (t: term n) : term n := + match t with + | App (Abs _ f) arg => bind (bind_first (par_max arg)) (par_max f) + | Srt _ | Var _ => t + | Pi A B => Pi (par_max A) (par_max B) + | Abs T f => Abs (par_max T) (par_max f) + | App a b => App (par_max a) (par_max b) + end. + +Lemma par_par_max {n} (t: term n) : t ⪼ par_max t. + induction t; simpl; try solve [constructor; assumption]. + destruct t1; try solve [constructor; assumption]. + simpl in *. inversion_clear IHt1. + constructor; assumption. +Qed. + +Lemma ren_preserves_par {n k} (σ: {i | i < n} -> {i | i < k}) t u : + t ⪼ u -> ren σ t ⪼ ren σ u. +Proof. + induction 1 in k, σ |- *; simpl; try constructor; auto. + rewrite ren_bind. specialize (IHpar_step1 _ (lift σ)). specialize (IHpar_step2 _ σ). + enough ( + e : bind (ren σ ∘ bind_first arg') f' = + bind (bind_first (ren σ arg')) (ren (lift σ) f') + ) by (rewrite e; constructor; assumption). clear. rewrite bind_ren. + apply bind_ext. + intro. unfold lift, bind_first. destruct (lt_dec _ _); simpl. + - pose proof (proj2_sig (σ (exist _ (proj1_sig i) l))). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + - destruct (lt_dec _ _); try lia. reflexivity. +Qed. + +Lemma par_max_is_max {n} (t t': term n) : t ⪼ t' -> t' ⪼ par_max t. +Proof. + induction 1; simpl in *; try solve [constructor; assumption]. + - destruct t1; try solve [constructor; assumption]. + simpl in *. inversion H; subst; clear H. inversion_clear IHpar_step1. + constructor; assumption. + - revert IHpar_step1 IHpar_step2. clear. generalize (par_max f), (par_max arg). clear. + rename f' into f, arg' into arg. intros f' arg' fred argred. + cut (forall i, bind_first arg i ⪼ bind_first arg' i); swap 1 2. + { unfold bind_first. intro. destruct (lt_dec _ _); try assumption; constructor. } + generalize (bind_first arg) as σ1, (bind_first arg') as σ2. + clear arg arg' argred. generalize dependent n. fix IH 4. + destruct 1; simpl. + + intros ? ? H. apply H. + + constructor. + + constructor; auto. apply IH; try assumption. unfold lift_bind. + intro. destruct (lt_dec _ _); try solve [constructor]. + apply ren_preserves_par. apply H. + + constructor; auto. apply IH; try assumption. unfold lift_bind. + intro. destruct (lt_dec _ _); try solve [constructor]. + apply ren_preserves_par. apply H. + + constructor; auto. + + intros. rewrite bind_comp. + apply IH with (σ1 := lift_bind σ1) (σ2 := lift_bind σ2) in fred1 as IHf; swap 1 2. + { unfold lift_bind. intro. destruct (lt_dec _ _); try solve [constructor]. + apply ren_preserves_par. apply H. } + apply IH with (σ1 := σ1) (σ2 := σ2) in fred2 as IHarg; try assumption. + enough ( + e : bind (bind σ2 ∘ bind_first arg') f' = + bind (bind_first (bind σ2 arg')) (bind (lift_bind σ2) f') + ) by (rewrite e; constructor; try assumption). + rewrite bind_comp. apply bind_ext. + intro. unfold lift_bind, bind_first at 1. + destruct (lt_dec _ _). + * simpl. rewrite bind_ren. + generalize (σ2 (exist _ (proj1_sig i) l)). + intro. clear. assert (forall i, (bind_first (bind σ2 arg') ∘ weaken) i = Var i). + { intro. unfold weaken. unfold bind_first. simpl. pose proof (proj2_sig i). + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. } + revert H. generalize (bind_first (bind σ2 arg') ∘ weaken). clear. + induction t; simpl; auto; intros; f_equal; auto; apply IHt2. + -- unfold lift_bind. intro. destruct (lt_dec _ _). + ++ rewrite H. simpl. unfold weaken. f_equal. apply sig_lt_ext. reflexivity. + ++ f_equal. apply sig_lt_ext. pose proof (proj2_sig i). simpl in *. lia. + -- unfold lift_bind. intro. destruct (lt_dec _ _). + ++ rewrite H. simpl. unfold weaken. f_equal. apply sig_lt_ext. reflexivity. + ++ f_equal. apply sig_lt_ext. pose proof (proj2_sig i). simpl in *. lia. + * simpl. unfold bind_first. simpl. destruct (lt_dec n n); try lia. reflexivity. +Qed. + +Lemma diamond_par {n} (t u u': term n) : t ⪼ u -> t ⪼ u' -> exists v, u ⪼ v /\ u' ⪼ v. + intros. exists (par_max t). split; apply par_max_is_max; assumption. +Qed. + +Lemma left_star_par_commute {n} (t u u': term n) : t ⪼* u -> t ⪼ u' -> exists v, u ⪼ v /\ u' ⪼* v. +Proof. + destruct 1. { intro. exists u'. intuition. constructor. } + induction H in u' |- *. + - intro redr. specialize (IHRplus _ redr) as IHu'. destruct IHu' as [x []]. + destruct (diamond_par m b x); try assumption. intuition. exists x0. intuition. + destruct H2. + + do 2 constructor. assumption. + + constructor. econstructor; eassumption. + - intro. destruct (diamond_par t b u'); try assumption. exists x. intuition. do 2 constructor. + assumption. +Qed. + +Lemma confluence_par {n} (t u u': term n) : t ⪼* u -> t ⪼* u' -> exists v, u ⪼* v /\ u' ⪼* v. +Proof. + destruct 2. { eexists. intuition try eassumption. constructor. } + induction H0; firstorder. + - destruct (left_star_par_commute _ _ _ H3 H1). exists x0. intuition. constructor. destruct H2. + + constructor. assumption. + + econstructor; eassumption. + - destruct (left_star_par_commute _ _ _ H H0). exists x. intuition. do 2 constructor. assumption. +Qed. + +Lemma step_incl_par {n} (t u: term n) : t ≻ u -> t ⪼ u. +Proof. + destruct 1. + induction K; simpl; try solve [constructor; auto using par_refl]. + destruct H. constructor; apply par_refl. +Qed. + +Lemma step_star_incl_par_star {n} (t u: term n) : t ≻* u -> t ⪼* u. +Proof. + destruct 1; constructor. + induction H. + - econstructor; try eassumption. apply step_incl_par. assumption. + - constructor. apply step_incl_par. assumption. +Qed. + +Lemma par_incl_step_star {n} (t u: term n) : t ⪼ u -> t ≻* u. + induction 1; try solve [constructor]. + - eapply Rstar_trans. + + change (Pi t1 t2) with (fill (PiL Hole t2) t1). apply step_star_context. eassumption. + + simpl. change (Pi u1 ?x) with (fill (PiR u1 Hole) x). apply step_star_context. assumption. + - eapply Rstar_trans. + + change (Abs t1 t2) with (fill (AbsL Hole t2) t1). apply step_star_context. eassumption. + + simpl. change (Abs u1 ?x) with (fill (AbsR u1 Hole) x). apply step_star_context. assumption. + - eapply Rstar_trans. + + change (App t1 t2) with (fill (AppL Hole t2) t1). apply step_star_context. eassumption. + + simpl. change (App u1 ?x) with (fill (AppR u1 Hole) x). apply step_star_context. assumption. + - apply Rstar_trans with (y := App (Abs T f') arg). + + change (App (Abs T ?x) ?y) with (fill (AppL (AbsR T Hole) y) x). + apply step_star_context. assumption. + + apply Rstar_trans with (y := App (Abs T f') arg'). + * change (App ?x ?y) with (fill (AppR x Hole) y). apply step_star_context. assumption. + * do 2 constructor. change (?x ≻ ?y) with (fill Hole x ≻ fill Hole y). do 2 constructor. +Qed. + +Lemma par_star_incl_step_star {n} (t u: term n) : t ⪼* u -> t ≻* u. +Proof. + destruct 1; [constructor |]. + induction H. + - eapply Rstar_trans; try eassumption. apply par_incl_step_star. assumption. + - apply par_incl_step_star. assumption. +Qed. + +Lemma confluence_step {n} (t u u': term n) : t ≻* u -> t ≻* u' -> exists v, u ≻* v /\ u' ≻* v. +Proof. + intros tl tr. apply step_star_incl_par_star in tl, tr. + destruct (confluence_par _ _ _ tl tr) as [v]. exists v. intuition auto using par_star_incl_step_star. +Qed. diff --git a/theories/LambdaCube/Term.v b/theories/LambdaCube/Term.v index 06d4558..baeeb62 100644 --- a/theories/LambdaCube/Term.v +++ b/theories/LambdaCube/Term.v @@ -25,22 +25,22 @@ Arguments App {n}. Arguments Srt {n}. (* Execution contexts of the Lambda Cube with n free variables. *) -Inductive ctx (n : nat) : Type := -| Hole : ctx n -| PiL : ctx n → term (S n) → ctx n -| AbsL : ctx n → term (S n) → ctx n -| AppL : ctx n → term n → ctx n -| PiR : term n → ctx (S n) → ctx n -| AbsR : term n → ctx (S n) → ctx n -| AppR : term n → ctx n → ctx n. +Inductive ctx (n : nat) : nat -> Type := +| Hole : ctx n n +| PiL k : ctx n k → term (S n) → ctx n k +| AbsL k : ctx n k → term (S n) → ctx n k +| AppL k : ctx n k → term n → ctx n k +| PiR k : term n → ctx (S n) (S k) → ctx n (S k) +| AbsR k : term n → ctx (S n) (S k) → ctx n (S k) +| AppR k : term n → ctx n k → ctx n k. Arguments Hole {n}. -Arguments PiL {n}. -Arguments AbsL {n}. -Arguments AppL {n}. -Arguments PiR {n}. -Arguments AbsR {n}. -Arguments AppR {n}. +Arguments PiL {n k}. +Arguments AbsL {n k}. +Arguments AppL {n k}. +Arguments PiR {n k}. +Arguments AbsR {n k}. +Arguments AppR {n k}. Lemma sig_lt_ext {k : nat} (p q : {i | i < k}) : proj1_sig p = proj1_sig q → p = q. @@ -52,6 +52,16 @@ Proof. apply le_unique. Qed. +Lemma ctx_le n k : ctx n k -> n <= k. +Proof. + induction 1; lia. +Qed. + +Lemma not_ctx_S_0 {n} : ctx (S n) 0 -> False. +Proof. + intro K. apply ctx_le in K. lia. +Qed. + (* Basic weakening renaming *) Definition weaken {k : nat} (i : {i | i < k}) : {i | i < S k} := exist _ (proj1_sig i) (Nat.lt_lt_succ_r _ _ (proj2_sig i)). @@ -143,28 +153,38 @@ Fixpoint ren {k n : nat} (σ : {i | i < k} → {i | i < n}) (t : term k) : term | Srt s => Srt s end. -(* Renaming of free variables in a context *) -Fixpoint renK {k n : nat} (σ : {i | i < k} → {i | i < n}) (K : ctx k) : ctx n := - match K with - | Hole => Hole - | PiL K fam => PiL (renK σ K) (ren (lift σ) fam) - | AbsL K tm => AbsL (renK σ K) (ren (lift σ) tm) - | AppL K tm2 => AppL (renK σ K) (ren σ tm2) - | PiR ty K => PiR (ren σ ty) (renK (lift σ) K) - | AbsR ty K => AbsR (ren σ ty) (renK (lift σ) K) - | AppR tm1 K => AppR (ren σ tm1) (renK σ K) +(* Plug a term in place of the hole in a context *) +Fixpoint fill {n k : nat} (K : ctx n k) : term k -> term n := + match K in ctx _ k return term k -> term n with + | Hole => fun t => t + | PiL K fam => fun t => Pi (fill K t) fam + | AbsL K tm => fun t => Abs (fill K t) tm + | AppL K tm => fun t => App (fill K t) tm + | PiR ty K => fun t => Pi ty (fill K t) + | AbsR ty K => fun t => Abs ty (fill K t) + | AppR tm K => fun t => App tm (fill K t) end. -(* Plug a term in place of the hole in a context *) -Fixpoint fill {n : nat} (K : ctx n) (t : term n) : term n := - match K with - | Hole => t - | PiL K fam => Pi (fill K t) fam - | AbsL K tm => Abs (fill K t) tm - | AppL K tm => App (fill K t) tm - | PiR ty K => Pi ty (fill K (ren weaken t)) - | AbsR ty K => Abs ty (fill K (ren weaken t)) - | AppR tm K => App tm (fill K t) +(* Plug a context in place of the hole in a context *) +Fixpoint fillK {k n m : nat} (K : ctx m n) : ctx n k -> ctx m k := + match K in ctx _ x return ctx x k -> ctx m k with + | Hole => fun K' => K' + | PiL K fam => fun K' => PiL (fillK K K') fam + | AbsL K tm => fun K' => AbsL (fillK K K') tm + | AppL K tm => fun K' => AppL (fillK K K') tm + | PiR ty K => + fun K' => + match k as k return ctx (S m) k -> ctx m k with + | 0 => fun K => match not_ctx_S_0 K with end + | S k => fun K => PiR ty K + end (fillK K K') + | AbsR ty K => + fun K' => + match k as k return ctx (S m) k -> ctx m k with + | 0 => fun K => match not_ctx_S_0 K with end + | S k => fun K => AbsR ty K + end (fillK K K') + | AppR tm K => fun K' => AppR tm (fillK K K') end. Lemma ren_ext : @@ -203,23 +223,11 @@ Proof. now rewrite !IH. Qed. -Lemma ren_fill : - ∀ {k n : nat} - (σ : {i | i < k} → {i | i < n}) - (K : ctx k) (t : term k), - ren σ (fill K t) = fill (renK σ K) (ren σ t). +Lemma fill_fillK {k n m : nat} (K : ctx m n) (K': ctx n k) t : + fill (fillK K K') t = fill K (fill K' t). Proof. - fix IH 4. - intros k n σ K t. - destruct K; simpl; try congruence. - all: - f_equal; - rewrite IH; - f_equal; - rewrite !ren_comp; - apply ren_ext; - intros i; - apply lift_weaken. + induction K; simpl; try congruence; destruct k; try solve [destruct (not_ctx_S_0 _)]; simpl; + f_equal; rewrite IHK; f_equal; symmetry; apply ren_fill. Qed. (* Lifting of variable substitutions *) @@ -269,18 +277,6 @@ Fixpoint bind {k n : nat} (σ : {i | i < k} → term n) (t : term k) : term n | Srt s => Srt s end. -(* Substitution of free variables inside a context *) -Fixpoint bindK {k n : nat} (σ : {i | i < k} → term n) (K : ctx k) : ctx n := - match K with - | Hole => Hole - | PiL K fam => PiL (bindK σ K) (bind (lift_bind σ) fam) - | AbsL K tm => AbsL (bindK σ K) (bind (lift_bind σ) tm) - | AppL K tm2 => AppL (bindK σ K) (bind σ tm2) - | PiR ty K => PiR (bind σ ty) (bindK (lift_bind σ) K) - | AbsR ty K => AbsR (bind σ ty) (bindK (lift_bind σ) K) - | AppR tm1 K => AppR (bind σ tm1) (bindK σ K) - end. - Lemma bind_ext : ∀ {k n : nat} (σ1 σ2: {i | i < k} → term n) @@ -454,23 +450,6 @@ Proof. now rewrite !IH. Qed. -Lemma bind_fill : - ∀ {k n : nat} - (σ : {i | i < k} → term n) - (K : ctx k) (t : term k), - bind σ (fill K t) = fill (bindK σ K) (bind σ t). -Proof. - fix IH 4. - intros k n σ K t. - destruct K; simpl; try congruence. - all: rewrite IH; - do 2 f_equal; - rewrite bind_ren, - ren_bind; - apply bind_ext; - apply lift_bind_weaken. -Qed. - (* Basic substitution capturing the free variable introduced last *) Definition bind_first {k : nat} (t : term k) (i : {i | i < S k}) : term k := From 31bbba5b13bcb64c61a158cb27d91c93577a19f6 Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Sun, 16 Nov 2025 21:07:58 +0100 Subject: [PATCH 10/21] added typing --- theories/LambdaCube/Operational.v | 2 + theories/LambdaCube/Typing.v | 116 ++++++++++++++++++++++++++++++ 2 files changed, 118 insertions(+) create mode 100644 theories/LambdaCube/Typing.v diff --git a/theories/LambdaCube/Operational.v b/theories/LambdaCube/Operational.v index 58fbd58..a19bfc8 100644 --- a/theories/LambdaCube/Operational.v +++ b/theories/LambdaCube/Operational.v @@ -71,6 +71,8 @@ Inductive Requiv {A} (R: relation A) a : A -> Prop := | Rclot_plus_equiv_r b : Rplus R b a -> Requiv R a b | Requiv_refl : Requiv R a a. +Notation "t ≅ u" := (Requiv step t u). + Reserved Notation "t ⪼ u" (at level 70). Reserved Notation "t ⪼+ u" (at level 70). Reserved Notation "t ⪼* u" (at level 70). diff --git a/theories/LambdaCube/Typing.v b/theories/LambdaCube/Typing.v new file mode 100644 index 0000000..71164bb --- /dev/null +++ b/theories/LambdaCube/Typing.v @@ -0,0 +1,116 @@ +From Coq Require Import Utf8. +From Coq Require Import Arith Lia. +From FormArith Require Import Base. +From FormArith.LambdaCube Require Import Term Operational. + +Inductive typing_ctx n : nat -> Type := +| empty : typing_ctx n 0 +| cons {l} : typing_ctx n l -> term n -> typing_ctx n (S l). + +Arguments empty {n}. +Arguments cons {n l}. + +Notation "\" := empty. + +Fixpoint kth_index_ctx {n l} (Γ: typing_ctx n l) k {struct Γ} : k < l -> term n := + match Γ in typing_ctx _ l return k < l -> term n with + | \ => fun H => match Nat.nlt_0_r _ H with end + | @cons _ l Γ t => + match k return k < S l -> term n with + | 0 => fun _ => t + | S k => fun (H: S k < S l) => kth_index_ctx Γ k (le_S_n _ _ H) + end + end +. + +Fixpoint map_ctx {n m l} (f: term n -> term m) (Γ: typing_ctx n l) : typing_ctx m l := + match Γ with + | \ => \ + | cons Γ t => cons (map_ctx f Γ) (f t) + end. + +Definition slide {n} (i : {k | k < n}) : {k | k < S n} := + exist _ (S (proj1_sig i)) (le_n_S _ _ (proj2_sig i)). + +Definition cons' {n} (Γ : typing_ctx n n) (t: term n) : typing_ctx (S n) (S n) := + cons (map_ctx (ren slide) Γ) (ren slide t). + +Notation "A , t" := (cons' A t) (at level 61, left associativity, t at next level). + +Definition pi_scheme := sort -> sort -> bool. + +Definition pi_scheme_check (P: pi_scheme) (s s': sort) : Prop := P s s' = true. + +Reserved Notation "A ⊢( P ) s ':' t" + (at level 70, s at next level, t at next level, P at next level). +Reserved Notation "A ⊢( P )" (at level 70, P at next level). + +Inductive typing (P: pi_scheme) : forall {n}, typing_ctx n n -> term n -> term n -> Prop := +| typ_star {n} {Γ: typing_ctx n n} : Γ ⊢(P) -> Γ ⊢(P) Srt Star : Srt Box +| typ_var {n} {Γ: typing_ctx n n} {i} : + Γ ⊢(P) -> Γ ⊢(P) Var i : kth_index_ctx Γ (proj1_sig i) (proj2_sig i) +| typ_pi {n} {Γ: typing_ctx n n} {A B s s'} : + pi_scheme_check P s s' -> Γ ⊢(P) A : Srt s -> Γ, A ⊢(P) B : Srt s' -> Γ ⊢(P) Pi A B : Srt s' +| typ_abs {n} {Γ: typing_ctx n n} {A B s s' t} : + pi_scheme_check P s s' -> + Γ ⊢(P) A : Srt s -> + Γ, A ⊢(P) B : Srt s' -> + Γ, A ⊢(P) t : B -> + Γ ⊢(P) Abs A t : Pi A B +| typ_app {n} {Γ: typing_ctx n n} {A B t u} : + Γ ⊢(P) t : Pi A B -> Γ ⊢(P) u : A -> Γ ⊢(P) App t u : bind (bind_first u) B +| typ_conv {n} {Γ: typing_ctx n n} {t A B} : + Γ ⊢(P) t : A -> A ≅ B -> Γ ⊢(P) t : B +with ctx_wf (P: pi_scheme) : forall {n}, typing_ctx n n -> Prop := +| empty_wf : \ ⊢(P) +| cons_wf {n} {A: typing_ctx n n} {t: term n} {s} : + A ⊢(P) -> A ⊢(P) t : Srt s -> A, t ⊢(P) +where "A ⊢( P ) t ':' s" := (typing P A t s) +and "A ⊢( P )" := (ctx_wf P A) +. + +Definition is_star (s: sort) : bool := + match s with Star => true | Box => false end. + +Definition is_box (s: sort) : bool := + match s with Star => false | Box => true end. + +Open Scope bool. + +Definition simple_typed : pi_scheme := + fun s s' => is_star s && is_star s'. + +Notation "'λ→'" := simple_typed. + +Definition systemF : pi_scheme := + fun s s' => is_star s'. + +Notation "'F'" := systemF. + +Definition weak_omega : pi_scheme := + fun s s' => (is_star s && is_star s') || (is_box s && is_box s'). + +Notation "'wω'" := weak_omega. + +Definition systemP : pi_scheme := + fun s s' => is_star s. + +Notation "'P'" := systemP. + +Definition system_omega : pi_scheme := + fun s s' => is_box s || is_star s'. + +Definition systemPF : pi_scheme := + fun s s' => is_star s || is_star s'. + +Notation "'PF'" := systemP. + +Definition P_weak_omega : pi_scheme := + fun s s' => is_star s || is_box s'. + +Notation "'Pwω'" := P_weak_omega. + +Definition CoC : pi_scheme := + fun s s' => true. + +Notation "'C'" := CoC. From 9b5d5b19fbaf025b3b0b035cc0bec386b2446dd7 Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Mon, 17 Nov 2025 15:00:16 +0100 Subject: [PATCH 11/21] typing contexts are now parametrized by one integer and not 2 --- theories/LambdaCube/Typing.v | 61 ++++++++++++++---------------------- 1 file changed, 24 insertions(+), 37 deletions(-) diff --git a/theories/LambdaCube/Typing.v b/theories/LambdaCube/Typing.v index 71164bb..cd8db5e 100644 --- a/theories/LambdaCube/Typing.v +++ b/theories/LambdaCube/Typing.v @@ -3,40 +3,27 @@ From Coq Require Import Arith Lia. From FormArith Require Import Base. From FormArith.LambdaCube Require Import Term Operational. -Inductive typing_ctx n : nat -> Type := -| empty : typing_ctx n 0 -| cons {l} : typing_ctx n l -> term n -> typing_ctx n (S l). - -Arguments empty {n}. -Arguments cons {n l}. +Inductive typing_ctx : nat -> Type := +| empty : typing_ctx 0 +| cons {n} : typing_ctx n -> term n -> typing_ctx (S n). Notation "\" := empty. +Notation "A , t" := (cons A t) (at level 61, left associativity, t at next level). -Fixpoint kth_index_ctx {n l} (Γ: typing_ctx n l) k {struct Γ} : k < l -> term n := - match Γ in typing_ctx _ l return k < l -> term n with - | \ => fun H => match Nat.nlt_0_r _ H with end - | @cons _ l Γ t => - match k return k < S l -> term n with - | 0 => fun _ => t - | S k => fun (H: S k < S l) => kth_index_ctx Γ k (le_S_n _ _ H) - end - end -. +Search (_ < S _ -> {_} + {_}). -Fixpoint map_ctx {n m l} (f: term n -> term m) (Γ: typing_ctx n l) : typing_ctx m l := - match Γ with - | \ => \ - | cons Γ t => cons (map_ctx f Γ) (f t) +Fixpoint kth_index_ctx {n} (Γ: typing_ctx n) k {struct Γ} : k < n -> term n := + match Γ in typing_ctx n return k < n -> term n with + | \ => fun H => match Nat.nlt_0_r _ H with end + | @cons n Γ t => + fun _ => + ren weaken + match lt_dec k n with + | left H => kth_index_ctx Γ k H + | right _ => t + end end. -Definition slide {n} (i : {k | k < n}) : {k | k < S n} := - exist _ (S (proj1_sig i)) (le_n_S _ _ (proj2_sig i)). - -Definition cons' {n} (Γ : typing_ctx n n) (t: term n) : typing_ctx (S n) (S n) := - cons (map_ctx (ren slide) Γ) (ren slide t). - -Notation "A , t" := (cons' A t) (at level 61, left associativity, t at next level). - Definition pi_scheme := sort -> sort -> bool. Definition pi_scheme_check (P: pi_scheme) (s s': sort) : Prop := P s s' = true. @@ -45,25 +32,25 @@ Reserved Notation "A ⊢( P ) s ':' t" (at level 70, s at next level, t at next level, P at next level). Reserved Notation "A ⊢( P )" (at level 70, P at next level). -Inductive typing (P: pi_scheme) : forall {n}, typing_ctx n n -> term n -> term n -> Prop := -| typ_star {n} {Γ: typing_ctx n n} : Γ ⊢(P) -> Γ ⊢(P) Srt Star : Srt Box -| typ_var {n} {Γ: typing_ctx n n} {i} : +Inductive typing (P: pi_scheme) : forall {n}, typing_ctx n -> term n -> term n -> Prop := +| typ_star {n} {Γ: typing_ctx n} : Γ ⊢(P) -> Γ ⊢(P) Srt Star : Srt Box +| typ_var {n} {Γ: typing_ctx n} {i} : Γ ⊢(P) -> Γ ⊢(P) Var i : kth_index_ctx Γ (proj1_sig i) (proj2_sig i) -| typ_pi {n} {Γ: typing_ctx n n} {A B s s'} : +| typ_pi {n} {Γ: typing_ctx n} {A B s s'} : pi_scheme_check P s s' -> Γ ⊢(P) A : Srt s -> Γ, A ⊢(P) B : Srt s' -> Γ ⊢(P) Pi A B : Srt s' -| typ_abs {n} {Γ: typing_ctx n n} {A B s s' t} : +| typ_abs {n} {Γ: typing_ctx n} {A B s s' t} : pi_scheme_check P s s' -> Γ ⊢(P) A : Srt s -> Γ, A ⊢(P) B : Srt s' -> Γ, A ⊢(P) t : B -> Γ ⊢(P) Abs A t : Pi A B -| typ_app {n} {Γ: typing_ctx n n} {A B t u} : +| typ_app {n} {Γ: typing_ctx n} {A B t u} : Γ ⊢(P) t : Pi A B -> Γ ⊢(P) u : A -> Γ ⊢(P) App t u : bind (bind_first u) B -| typ_conv {n} {Γ: typing_ctx n n} {t A B} : +| typ_conv {n} {Γ: typing_ctx n} {t A B} : Γ ⊢(P) t : A -> A ≅ B -> Γ ⊢(P) t : B -with ctx_wf (P: pi_scheme) : forall {n}, typing_ctx n n -> Prop := +with ctx_wf (P: pi_scheme) : forall {n}, typing_ctx n -> Prop := | empty_wf : \ ⊢(P) -| cons_wf {n} {A: typing_ctx n n} {t: term n} {s} : +| cons_wf {n} {A: typing_ctx n} {t: term n} {s} : A ⊢(P) -> A ⊢(P) t : Srt s -> A, t ⊢(P) where "A ⊢( P ) t ':' s" := (typing P A t s) and "A ⊢( P )" := (ctx_wf P A) From 57f9c0a6554e04533d96f522265bf2bff8834c31 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Tue, 18 Nov 2025 16:30:36 +0100 Subject: [PATCH 12/21] Simplified execution contexts --- theories/LambdaCube/Operational.v | 2 +- theories/LambdaCube/Term.v | 85 ++++++++++++++----------------- 2 files changed, 38 insertions(+), 49 deletions(-) diff --git a/theories/LambdaCube/Operational.v b/theories/LambdaCube/Operational.v index a19bfc8..1e2fa92 100644 --- a/theories/LambdaCube/Operational.v +++ b/theories/LambdaCube/Operational.v @@ -17,7 +17,7 @@ Inductive head_step {n : nat} : term n → term n → Prop := where "t [≻] u" := (head_step t u). Inductive step {n : nat} : term n → term n → Prop := -| ctx_red {k} (K : ctx n k) (t u : term k) : +| ctx_red {k} (K : ctx k n) (t u : term k) : t [≻] u → fill K t ≻ fill K u where "t ≻ u" := (step t u). diff --git a/theories/LambdaCube/Term.v b/theories/LambdaCube/Term.v index baeeb62..49b4c89 100644 --- a/theories/LambdaCube/Term.v +++ b/theories/LambdaCube/Term.v @@ -25,22 +25,22 @@ Arguments App {n}. Arguments Srt {n}. (* Execution contexts of the Lambda Cube with n free variables. *) -Inductive ctx (n : nat) : nat -> Type := -| Hole : ctx n n -| PiL k : ctx n k → term (S n) → ctx n k -| AbsL k : ctx n k → term (S n) → ctx n k -| AppL k : ctx n k → term n → ctx n k -| PiR k : term n → ctx (S n) (S k) → ctx n (S k) -| AbsR k : term n → ctx (S n) (S k) → ctx n (S k) -| AppR k : term n → ctx n k → ctx n k. - -Arguments Hole {n}. -Arguments PiL {n k}. -Arguments AbsL {n k}. -Arguments AppL {n k}. -Arguments PiR {n k}. -Arguments AbsR {n k}. -Arguments AppR {n k}. +Inductive ctx (k : nat) : nat → Type := +| Hole : ctx k k +| PiL {n} : ctx k n → term (S n) → ctx k n +| AbsL {n} : ctx k n → term (S n) → ctx k n +| AppL {n} : ctx k n → term n → ctx k n +| PiR {n} : term n → ctx k (S n) → ctx k n +| AbsR {n} : term n → ctx k (S n)→ ctx k n +| AppR {n} : term n → ctx k n → ctx k n. + +Arguments Hole {k}. +Arguments PiL {k n}. +Arguments AbsL {k n}. +Arguments AppL {k n}. +Arguments PiR {k n}. +Arguments AbsR {k n}. +Arguments AppR {k n}. Lemma sig_lt_ext {k : nat} (p q : {i | i < k}) : proj1_sig p = proj1_sig q → p = q. @@ -52,12 +52,12 @@ Proof. apply le_unique. Qed. -Lemma ctx_le n k : ctx n k -> n <= k. +Lemma ctx_le n k : ctx k n -> n <= k. Proof. induction 1; lia. Qed. -Lemma not_ctx_S_0 {n} : ctx (S n) 0 -> False. +Lemma not_ctx_S_0 {n} : ctx 0 (S n) -> False. Proof. intro K. apply ctx_le in K. lia. Qed. @@ -154,37 +154,26 @@ Fixpoint ren {k n : nat} (σ : {i | i < k} → {i | i < n}) (t : term k) : term end. (* Plug a term in place of the hole in a context *) -Fixpoint fill {n k : nat} (K : ctx n k) : term k -> term n := - match K in ctx _ k return term k -> term n with - | Hole => fun t => t - | PiL K fam => fun t => Pi (fill K t) fam - | AbsL K tm => fun t => Abs (fill K t) tm - | AppL K tm => fun t => App (fill K t) tm - | PiR ty K => fun t => Pi ty (fill K t) - | AbsR ty K => fun t => Abs ty (fill K t) - | AppR tm K => fun t => App tm (fill K t) +Fixpoint fill {k n : nat} (K : ctx k n) (t : term k) : term n := + match K in ctx _ n with + | Hole => t + | PiL K fam => Pi (fill K t) fam + | AbsL K tm => Abs (fill K t) tm + | AppL K tm => App (fill K t) tm + | PiR ty K => Pi ty (fill K t) + | AbsR ty K => Abs ty (fill K t) + | AppR tm K => App tm (fill K t) end. -(* Plug a context in place of the hole in a context *) -Fixpoint fillK {k n m : nat} (K : ctx m n) : ctx n k -> ctx m k := - match K in ctx _ x return ctx x k -> ctx m k with - | Hole => fun K' => K' - | PiL K fam => fun K' => PiL (fillK K K') fam - | AbsL K tm => fun K' => AbsL (fillK K K') tm - | AppL K tm => fun K' => AppL (fillK K K') tm - | PiR ty K => - fun K' => - match k as k return ctx (S m) k -> ctx m k with - | 0 => fun K => match not_ctx_S_0 K with end - | S k => fun K => PiR ty K - end (fillK K K') - | AbsR ty K => - fun K' => - match k as k return ctx (S m) k -> ctx m k with - | 0 => fun K => match not_ctx_S_0 K with end - | S k => fun K => AbsR ty K - end (fillK K K') - | AppR tm K => fun K' => AppR tm (fillK K K') +Fixpoint fillK {k n m : nat} (K : ctx n m) (C : ctx k n) : ctx k m := + match K in ctx _ m0 return ctx k m0 with + | Hole => C + | PiL K fam => PiL (fillK K C) fam + | AbsL K tm => AbsL (fillK K C) tm + | AppL K tm => AppL (fillK K C) tm + | PiR ty K => PiR ty (fillK K C) + | AbsR ty K => AbsR ty (fillK K C) + | AppR tm K => AppR tm (fillK K C) end. Lemma ren_ext : @@ -223,7 +212,7 @@ Proof. now rewrite !IH. Qed. -Lemma fill_fillK {k n m : nat} (K : ctx m n) (K': ctx n k) t : +Lemma fill_fillK {k n m : nat} (K : ctx n m) (K': ctx k n) t : fill (fillK K K') t = fill K (fill K' t). Proof. induction K; simpl; try congruence; destruct k; try solve [destruct (not_ctx_S_0 _)]; simpl; From 75fa2999c62f16a0bc71a62f16c607f3c1176523 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Tue, 18 Nov 2025 17:55:36 +0100 Subject: [PATCH 13/21] Added stub of strong normalization proof --- theories/LambdaCube/SN.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 theories/LambdaCube/SN.v diff --git a/theories/LambdaCube/SN.v b/theories/LambdaCube/SN.v new file mode 100644 index 0000000..276d81f --- /dev/null +++ b/theories/LambdaCube/SN.v @@ -0,0 +1,11 @@ +From Coq Require Import Utf8. +From Coq Require Import Arith Lia. +From FormArith Require Import Base. +From FormArith.LambdaCube Require Import Term Operational Typing. + +Inductive SN {n : nat} (t : term n) : Prop := +| SN_on : (∀ u, t ≻ u → SN u) → SN t. + +Lemma typing_SN {Sc : pi_scheme} {n : nat} (Γ : typing_ctx n) (t A : term n) : + Γ ⊢(Sc) t : A → SN t. +Admitted. From 0e7d5bc7391d9e9da4bbef49eb0249fd45c2a40a Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Tue, 18 Nov 2025 23:10:13 +0100 Subject: [PATCH 14/21] proved subject reduction --- theories/LambdaCube/Operational.v | 363 +++++++++++++++++++++++++++++- theories/LambdaCube/Term.v | 16 ++ theories/LambdaCube/Typing.v | 258 ++++++++++++++++++++- 3 files changed, 631 insertions(+), 6 deletions(-) diff --git a/theories/LambdaCube/Operational.v b/theories/LambdaCube/Operational.v index a19bfc8..2181bbd 100644 --- a/theories/LambdaCube/Operational.v +++ b/theories/LambdaCube/Operational.v @@ -27,7 +27,7 @@ Proof. Qed. Inductive Rplus {A} (R: relation A) a b : Prop := -| add_last_R m : Rplus R a m -> R m b -> Rplus R a b +| add_last m : Rplus R a m -> R m b -> Rplus R a b | Rclot_plus : R a b -> Rplus R a b. Notation "t ≻+ u" := (Rplus step t u). @@ -67,12 +67,86 @@ Proof. Qed. Inductive Requiv {A} (R: relation A) a : A -> Prop := -| Rclot_plus_equiv b : Rplus R a b -> Requiv R a b -| Rclot_plus_equiv_r b : Rplus R b a -> Requiv R a b -| Requiv_refl : Requiv R a a. +| equiv_refl : Requiv R a a +| equiv_add_last b c : Requiv R a b -> R b c -> Requiv R a c +| equiv_add_last_r b c : Requiv R a b -> R c b -> Requiv R a c +. Notation "t ≅ u" := (Requiv step t u). +Lemma Requiv_clot {A} {R: relation A} {a b} : R a b -> Requiv R a b. +Proof. + intro. econstructor 2; try eassumption. constructor. +Qed. + +Lemma Requiv_clot_r {A} {R: relation A} {a b} : R a b -> Requiv R b a. +Proof. + intro. econstructor 3; try eassumption. constructor. +Qed. + +Lemma Requiv_add_first {A} {R: relation A} {a b c} : R a b -> Requiv R b c -> Requiv R a c. +Proof. + intro. induction 1. + - apply Requiv_clot. assumption. + - econstructor 2; eassumption. + - econstructor 3; eassumption. +Qed. + +Lemma Requiv_add_first_r {A} {R: relation A} {a b c} : R b a -> Requiv R b c -> Requiv R a c. +Proof. + intro. induction 1. + - apply Requiv_clot_r. assumption. + - econstructor 2; eassumption. + - econstructor 3; eassumption. +Qed. + +Lemma Requiv_sym {A} {R: relation A} {x y} : Requiv R x y -> Requiv R y x. +Proof. + induction 1. + - constructor. + - eapply Requiv_add_first_r; eassumption. + - eapply Requiv_add_first; eassumption. +Qed. + +Lemma Requiv_trans {A} {R: relation A} {x y z} : Requiv R x y -> Requiv R y z -> Requiv R x z. +Proof. + induction 2; auto. + - econstructor 2; eassumption. + - econstructor 3; eassumption. +Qed. + +Lemma Requiv_clot_plus {A} {R: relation A} {a b} : Rplus R a b -> Requiv R a b. +Proof. + induction 1. + - econstructor 2; eassumption. + - apply Requiv_clot. assumption. +Qed. + +Lemma Requiv_clot_plus_r {A} {R: relation A} {a b} : Rplus R a b -> Requiv R b a. +Proof. + intro. apply Requiv_sym, Requiv_clot_plus. assumption. +Qed. + +Lemma Requiv_clot_star {A} {R: relation A} {a b} : Rstar R a b -> Requiv R a b. +Proof. + destruct 1. + - constructor. + - apply Requiv_clot_plus. assumption. +Qed. + +Lemma Requiv_clot_star_r {A} {R: relation A} {a b} : Rstar R a b -> Requiv R b a. +Proof. + intro. apply Requiv_sym, Requiv_clot_star. assumption. +Qed. + +Lemma step_equiv_context {n k} (K: ctx n k) t u : t ≅ u -> fill K t ≅ fill K u. +Proof. + induction 1. + - constructor. + - econstructor; try eassumption. apply step_under_context. assumption. + - econstructor 3; try eassumption. apply step_under_context. assumption. +Qed. + Reserved Notation "t ⪼ u" (at level 70). Reserved Notation "t ⪼+ u" (at level 70). Reserved Notation "t ⪼* u" (at level 70). @@ -246,8 +320,287 @@ Proof. - apply par_incl_step_star. assumption. Qed. -Lemma confluence_step {n} (t u u': term n) : t ≻* u -> t ≻* u' -> exists v, u ≻* v /\ u' ≻* v. +Lemma confluence_step {n} {t u u': term n} : t ≻* u -> t ≻* u' -> exists v, u ≻* v /\ u' ≻* v. Proof. intros tl tr. apply step_star_incl_par_star in tl, tr. destruct (confluence_par _ _ _ tl tr) as [v]. exists v. intuition auto using par_star_incl_step_star. Qed. + +Lemma ren_preserves_redex {k n} (σ: {i | i < k} -> {i | i < n}) (t u: term k) : + t [≻] u -> ren σ t [≻] ren σ u. + destruct 1. simpl. + enough (e : ren σ (bind _ _) = _) by (rewrite e; constructor). + rewrite ren_bind. rewrite bind_ren. apply bind_ext. + intro. unfold bind_first at 1, lift. destruct (lt_dec _ _). + - unfold bind_first. simpl. pose proof (proj2_sig (σ (exist _ (proj1_sig i) l))). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + - unfold bind_first. simpl. destruct (lt_dec _ _); auto; lia. +Qed. + +Lemma ren_preserves_step {k n} (σ: {i | i < k} -> {i | i < n}) (t u: term k) : + t ≻ u -> ren σ t ≻ ren σ u. +Proof. + destruct 1. induction K in n, σ, t, u, H |- *; simpl. + - change (?x ≻ ?y) with (fill Hole x ≻ fill Hole y). constructor. apply ren_preserves_redex. + assumption. + - change (Pi ?x ?y) with (fill (PiL Hole y) x). apply step_under_context. auto. + - change (Abs ?x ?y) with (fill (AbsL Hole y) x). apply step_under_context. auto. + - change (App ?x ?y) with (fill (AppL Hole y) x). apply step_under_context. auto. + - change (Pi ?x ?y) with (fill (PiR x Hole) y). apply step_under_context. auto. + - change (Abs ?x ?y) with (fill (AbsR x Hole) y). apply step_under_context. auto. + - change (App ?x ?y) with (fill (AppR x Hole) y). apply step_under_context. auto. +Qed. + +Lemma ren_preserves_step_plus {k n} (σ: {i | i < k} -> {i | i < n}) (t u: term k) : + t ≻+ u -> ren σ t ≻+ ren σ u. +Proof. + induction 1. + - econstructor; try eassumption. apply ren_preserves_step. assumption. + - constructor. apply ren_preserves_step. assumption. +Qed. + +Lemma ren_preserves_step_star {k n} (σ: {i | i < k} -> {i | i < n}) (t u: term k) : + t ≻* u -> ren σ t ≻* ren σ u. + destruct 1. + - constructor. + - constructor. apply ren_preserves_step_plus. assumption. +Qed. + +Lemma ren_preserves_step_equiv {k n} (σ: {i | i < k} -> {i | i < n}) (t u: term k) : + t ≅ u -> ren σ t ≅ ren σ u. + induction 1. + - constructor. + - econstructor 2; try eassumption. apply ren_preserves_step. assumption. + - econstructor 3; try eassumption. apply ren_preserves_step. assumption. +Qed. + +Lemma bind_preserves_redex {k n} (σ: {i | i < k} -> term n) (t u: term k) : + t [≻] u -> bind σ t [≻] bind σ u. + destruct 1. simpl. + enough (e : bind σ (bind _ _) = _) by (rewrite e; constructor). + do 2 rewrite bind_comp. apply bind_ext. + intro. unfold bind_first at 1, lift_bind. destruct (lt_dec _ _); simpl. + - symmetry. rewrite bind_ren. apply bind_id. intro. unfold weaken, bind_first. simpl. + pose proof (proj2_sig k0). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + - unfold bind_first. simpl. destruct (lt_dec _ _); auto; lia. +Qed. + +Lemma bind_preserves_step {k n} (σ: {i | i < k} -> term n) (t u: term k) : + t ≻ u -> bind σ t ≻ bind σ u. +Proof. + destruct 1. induction K in n, σ, t, u, H |- *; simpl. + - change (?x ≻ ?y) with (fill Hole x ≻ fill Hole y). constructor. apply bind_preserves_redex. + assumption. + - change (Pi ?x ?y) with (fill (PiL Hole y) x). apply step_under_context. auto. + - change (Abs ?x ?y) with (fill (AbsL Hole y) x). apply step_under_context. auto. + - change (App ?x ?y) with (fill (AppL Hole y) x). apply step_under_context. auto. + - change (Pi ?x ?y) with (fill (PiR x Hole) y). apply step_under_context. auto. + - change (Abs ?x ?y) with (fill (AbsR x Hole) y). apply step_under_context. auto. + - change (App ?x ?y) with (fill (AppR x Hole) y). apply step_under_context. auto. +Qed. + +Lemma bind_preserves_step_plus {k n} (σ: {i | i < k} -> term n) (t u: term k) : + t ≻+ u -> bind σ t ≻+ bind σ u. +Proof. + induction 1. + - econstructor; try eassumption. apply bind_preserves_step. assumption. + - constructor. apply bind_preserves_step. assumption. +Qed. + +Lemma bind_preserves_step_star {k n} (σ: {i | i < k} -> term n) (t u: term k) : + t ≻* u -> bind σ t ≻* bind σ u. + destruct 1. + - constructor. + - constructor. apply bind_preserves_step_plus. assumption. +Qed. + +Lemma bind_preserves_step_equiv {k n} (σ: {i | i < k} -> term n) (t u: term k) : + t ≅ u -> bind σ t ≅ bind σ u. + induction 1. + - constructor. + - econstructor 2; try eassumption. apply bind_preserves_step. assumption. + - econstructor 3; try eassumption. apply bind_preserves_step. assumption. +Qed. + +Lemma bind_preserves_step_star_in_subs {k n} (σ1 σ2: {i | i < k} -> term n) (t: term k) : + (forall i, σ1 i ≻* σ2 i) -> bind σ1 t ≻* bind σ2 t. +Proof. + intro H. induction t in n, σ1, σ2, H |- *; simpl; auto. + - eapply Rstar_trans. + + change (Pi ?x ?y) with (fill (PiL Hole y) x). apply step_star_context. + eauto. + + simpl. change (Pi ?x ?y) with (fill (PiR x Hole) y). apply step_star_context. + apply IHt2. + unfold lift_bind. intro. destruct (lt_dec _ _). + * apply ren_preserves_step_star. apply H. + * constructor. + - eapply Rstar_trans. + + change (Abs ?x ?y) with (fill (AbsL Hole y) x). apply step_star_context. + eauto. + + simpl. change (Abs ?x ?y) with (fill (AbsR x Hole) y). apply step_star_context. + apply IHt2. + unfold lift_bind. intro. destruct (lt_dec _ _). + * apply ren_preserves_step_star. apply H. + * constructor. + - eapply Rstar_trans. + + change (App ?x ?y) with (fill (AppL Hole y) x). apply step_star_context. auto. + + simpl. change (App ?x ?y) with (fill (AppR x Hole) y). apply step_star_context. auto. + - constructor. +Qed. + +Lemma bind_preserves_step_equiv_in_subs {k n} (σ1 σ2: {i | i < k} -> term n) (t: term k) : + (forall i, σ1 i ≅ σ2 i) -> bind σ1 t ≅ bind σ2 t. +Proof. + intro H. induction t in n, σ1, σ2, H |- *; simpl; auto. + - eapply Requiv_trans. + + change (Pi ?x ?y) with (fill (PiL Hole y) x). apply step_equiv_context. + eauto. + + simpl. change (Pi ?x ?y) with (fill (PiR x Hole) y). apply step_equiv_context. + apply IHt2. + unfold lift_bind. intro. destruct (lt_dec _ _). + * apply ren_preserves_step_equiv. apply H. + * constructor. + - eapply Requiv_trans. + + change (Abs ?x ?y) with (fill (AbsL Hole y) x). apply step_equiv_context. + eauto. + + simpl. change (Abs ?x ?y) with (fill (AbsR x Hole) y). apply step_equiv_context. + apply IHt2. + unfold lift_bind. intro. destruct (lt_dec _ _). + * apply ren_preserves_step_equiv. apply H. + * constructor. + - eapply Requiv_trans. + + change (App ?x ?y) with (fill (AppL Hole y) x). apply step_equiv_context. auto. + + simpl. change (App ?x ?y) with (fill (AppR x Hole) y). apply step_equiv_context. auto. + - constructor. +Qed. + +Lemma equiv_both_star {n} {t t': term n} : t ≅ t' -> exists v, t ≻* v /\ t' ≻* v. +Proof. + induction 1. + - exists t. split; constructor. + - destruct IHRequiv as [v [redt redb]]. + epose proof (Hconfl := confluence_step redb). destruct Hconfl as [v' [redv redc]]. + + constructor 2. constructor. eassumption. + + exists v'. intuition. eapply Rstar_trans; eassumption. + - destruct IHRequiv as [v [redt redb]]. exists v. intuition. eapply Rstar_trans; try eassumption. + do 2 constructor. assumption. +Qed. + +Lemma no_srt_step {n} {s} {t : term n} : ¬ (Srt s ≻ t). +Proof. + inversion 1; subst; clear H. destruct K; try discriminate. simpl in *. subst. inversion H1. +Qed. + +Lemma srt_star {n} {s} {t: term n} : Srt s ≻* t -> t = Srt s. +Proof. + destruct 1; auto. + exfalso. induction H; auto. eapply no_srt_step; eassumption. +Qed. + +Lemma srt_equiv {n} {s} {t: term n} : Srt s ≅ t -> t ≻* Srt s. + intro. apply equiv_both_star in H. destruct H as [v [H res]]. + apply srt_star in H. subst. assumption. +Qed. + +Lemma srt_equiv_srt {n} {s s'} : @Srt n s ≅ Srt s' -> s = s'. +Proof. + intro H. apply srt_equiv in H. apply srt_star in H. congruence. +Qed. + +Lemma no_var_step {n} {i} {t: term n} : ¬ (Var i ≻ t). +Proof. + inversion 1; subst; clear H. destruct K; try discriminate. simpl in *. subst. inversion H1. +Qed. + +Lemma var_star {n} {i} {t: term n} : Var i ≻* t -> t = Var i. +Proof. + destruct 1; auto. + exfalso. induction H; auto. eapply no_var_step; eassumption. +Qed. + +Lemma var_equiv {n} {i} {t: term n} : Var i ≅ t -> t ≻* Var i. + intro. apply equiv_both_star in H. destruct H as [v [H res]]. + apply var_star in H. subst. assumption. +Qed. + +Lemma var_equiv_var {n} {i i'} : @Var n i ≅ Var i' -> i = i'. +Proof. + intro. apply var_equiv in H. apply var_star in H. congruence. +Qed. + +Lemma pi_step {n} {A t: term n} {B} : + Pi A B ≻ t -> (exists A', A ≻ A' /\ t = Pi A' B) \/ (exists B', B ≻ B' /\ t = Pi A B'). +Proof. + inversion 1; subst; clear H. destruct K; try discriminate; simpl in H0; subst. + - inversion H1. + - inversion H0; subst. left. eexists (fill K _). intuition eauto. constructor. assumption. + - inversion H0; subst. right. eexists (fill K _). intuition eauto. constructor. assumption. +Qed. + +Lemma pi_star {n} {A B} {t: term n} : Pi A B ≻* t -> exists A' B', A ≻* A' /\ B ≻* B' /\ t = Pi A' B'. +Proof. + destruct 1; eauto using @Rstar. + induction H. + - firstorder subst. apply pi_step in H0. firstorder subst. + + exists x1, x0. intuition. eapply Rstar_trans; eauto. do 2 constructor. assumption. + + exists x, x1. intuition. eapply Rstar_trans; eauto. do 2 constructor. assumption. + - apply pi_step in H. firstorder subst. + + do 2 eexists; intuition eauto. + * do 2 constructor. assumption. + * constructor. + + do 2 eexists; intuition eauto. + * constructor. + * do 2 constructor. assumption. +Qed. + +Lemma pi_equiv {n} {A B} {t: term n} : Pi A B ≅ t -> exists A' B', A ≅ A' /\ B ≅ B' /\ t ≻* Pi A' B'. + intro. apply equiv_both_star in H. destruct H as [v [H res]]. + apply pi_star in H. firstorder subst. do 2 eexists; intuition eauto using Requiv_clot_star. +Qed. + +Lemma pi_equiv_pi {n} {A : term n} {A' B B'} : Pi A B ≅ Pi A' B' -> A ≅ A' /\ B ≅ B'. +Proof. + intro H. apply pi_equiv in H as [Av [Bv [Aequiv [Bequiv H]]]]. + apply pi_star in H. destruct H as [Av' [Bv' [A'star [B'star e]]]]. + inversion e; subst; clear e. + split; eapply Requiv_trans; try eassumption; apply Requiv_clot_star_r; assumption. +Qed. + +Lemma abs_step {n} {A t: term n} {f} : + Abs A f ≻ t -> (exists A', A ≻ A' /\ t = Abs A' f) \/ (exists f', f ≻ f' /\ t = Abs A f'). +Proof. + inversion 1; subst; clear H. destruct K; try discriminate; simpl in H0; subst. + - inversion H1. + - inversion H0; subst. left. eexists (fill K _). intuition eauto. constructor. assumption. + - inversion H0; subst. right. eexists (fill K _). intuition eauto. constructor. assumption. +Qed. + +Lemma abs_star {n} {A f} {t: term n} : Abs A f ≻* t -> exists A' f', A ≻* A' /\ f ≻* f' /\ t = Abs A' f'. +Proof. + destruct 1; eauto using @Rstar. + induction H. + - firstorder subst. apply abs_step in H0. firstorder subst. + + exists x1, x0. intuition. eapply Rstar_trans; eauto. do 2 constructor. assumption. + + exists x, x1. intuition. eapply Rstar_trans; eauto. do 2 constructor. assumption. + - apply abs_step in H. firstorder subst. + + do 2 eexists; intuition eauto. + * do 2 constructor. assumption. + * constructor. + + do 2 eexists; intuition eauto. + * constructor. + * do 2 constructor. assumption. +Qed. + +Lemma abs_equiv {n} {A f} {t: term n} : Abs A f ≅ t -> exists A' f', A ≅ A' /\ f ≅ f' /\ t ≻* Abs A' f'. + intro. apply equiv_both_star in H. destruct H as [v [H res]]. + apply abs_star in H. firstorder subst. do 2 eexists; intuition eauto using Requiv_clot_star. +Qed. + +Lemma abs_equiv_abs {n} {A : term n} {A' f f'} : Abs A f ≅ Abs A' f' -> A ≅ A' /\ f ≅ f'. +Proof. + intro H. apply abs_equiv in H as [Av [fv [Aequiv [fequiv H]]]]. + apply abs_star in H. destruct H as [Av' [fv' [A'star [f'star e]]]]. + inversion e; subst; clear e. + split; eapply Requiv_trans; try eassumption; apply Requiv_clot_star_r; assumption. +Qed. diff --git a/theories/LambdaCube/Term.v b/theories/LambdaCube/Term.v index baeeb62..d21a8b1 100644 --- a/theories/LambdaCube/Term.v +++ b/theories/LambdaCube/Term.v @@ -294,6 +294,22 @@ Proof. all : apply IH, lift_bind_ext, σ_eq. Qed. +Lemma bind_id : + ∀ {n} (σ : {i | i < n} -> term n) (t: term n), (forall k, σ k = Var k) -> bind σ t = t. + induction t; simpl; auto. + - intro. f_equal. + + apply IHt1. assumption. + + apply IHt2. unfold lift_bind. intro. destruct (lt_dec _ _). + * rewrite H. simpl. f_equal. apply sig_lt_ext. reflexivity. + * f_equal. apply sig_lt_ext. simpl. pose proof (proj2_sig k); simpl in *. lia. + - intro. f_equal. + + apply IHt1. assumption. + + apply IHt2. unfold lift_bind. intro. destruct (lt_dec _ _). + * rewrite H. simpl. f_equal. apply sig_lt_ext. reflexivity. + * f_equal. apply sig_lt_ext. simpl. pose proof (proj2_sig k); simpl in *. lia. + - intro. f_equal; auto. +Qed. + Lemma lift_bind_lift : ∀ {k m n : nat} (σ1 : {i | i < k} → {i | i < m}) diff --git a/theories/LambdaCube/Typing.v b/theories/LambdaCube/Typing.v index cd8db5e..347aac3 100644 --- a/theories/LambdaCube/Typing.v +++ b/theories/LambdaCube/Typing.v @@ -90,7 +90,7 @@ Definition system_omega : pi_scheme := Definition systemPF : pi_scheme := fun s s' => is_star s || is_star s'. -Notation "'PF'" := systemP. +Notation "'PF'" := systemPF. Definition P_weak_omega : pi_scheme := fun s s' => is_star s || is_box s'. @@ -101,3 +101,259 @@ Definition CoC : pi_scheme := fun s s' => true. Notation "'C'" := CoC. + +Lemma typ_star_inv Sc {n} (Γ : typing_ctx n) t : Γ ⊢(Sc) Srt Star : t -> t ≅ Srt Box. +Proof. + remember (Srt Star). induction 1; try discriminate; try solve [constructor]. + intuition subst. eapply Requiv_trans; try eassumption. apply Requiv_sym. assumption. +Qed. + +Lemma typ_var_inv Sc {n} (Γ : typing_ctx n) i T : + (Γ ⊢(Sc) Var i : T) -> T ≅ kth_index_ctx Γ (proj1_sig i) (proj2_sig i). + remember (Var i). induction 1 in i, Heqt |- *; try discriminate. + - inversion Heqt. subst. constructor. + - subst. specialize (IHtyping _ eq_refl). eapply Requiv_trans; eauto using Requiv_sym. +Qed. + +Lemma typ_pi_inv Sc {n} (Γ : typing_ctx n) A B T : + Γ ⊢(Sc) Pi A B : T -> exists s s', + T ≅ Srt s' /\ Γ ⊢(Sc) A : Srt s /\ Γ, A ⊢(Sc) B : Srt s' /\ pi_scheme_check Sc s s'. +Proof. + remember (Pi A B). induction 1 in A, B, Heqt |- *; try discriminate. + - exists s. exists s'. inversion Heqt; subst; clear Heqt. intuition constructor. + - subst. specialize (IHtyping _ _ eq_refl). destruct IHtyping as [s [s']]. + exists s. exists s'. intuition. eauto using Requiv_trans, Requiv_sym. +Qed. + +Lemma typ_abs_inv Sc {n} (Γ: typing_ctx n) A t T : + Γ ⊢(Sc) Abs A t : T -> + exists s s' B, + T ≅ Pi A B /\ Γ ⊢(Sc) A : Srt s /\ Γ, A ⊢(Sc) B : Srt s' /\ Γ, A ⊢(Sc) t : B /\ + pi_scheme_check Sc s s'. +Proof. + remember (Abs A t). + induction 1 in A, t, Heqt0 |- *; try discriminate. + - clear IHtyping1 IHtyping2 IHtyping3. inversion Heqt0. subst. clear Heqt0. + exists s. exists s'. exists B. intuition constructor. + - subst. specialize (IHtyping A t eq_refl). + destruct IHtyping as [s [s' [B0]]]. + exists s. exists s'. exists B0. intuition eauto using Requiv_trans, Requiv_sym. +Qed. + +Lemma typ_app_inv Sc {n} (Γ: typing_ctx n) t u T : + Γ ⊢(Sc) App t u : T -> exists A B, T ≅ bind (bind_first u) B /\ Γ ⊢(Sc) t : Pi A B /\ Γ ⊢(Sc) u : A. +Proof. + remember (App t u) as t0. + induction 1 in t, u, Heqt0 |- *; try discriminate. + - clear IHtyping1 IHtyping2. exists A, B. inversion Heqt0; subst; clear Heqt0. intuition constructor. + - subst. specialize (IHtyping _ _ eq_refl). + destruct IHtyping as [A0 [B0]]. + exists A0, B0. intuition eauto using Requiv_trans, Requiv_sym. +Qed. + +Lemma typing_imp_ctx_wf Sc {n} (Γ: typing_ctx n) t s : Γ ⊢(Sc) t : s -> Γ ⊢(Sc). +Proof. + induction 1; try assumption. +Qed. + +Lemma equiv_context (Sc : pi_scheme) {n} (Γ Γ': typing_ctx n) t s : + (forall k H, kth_index_ctx Γ' k H ≅ kth_index_ctx Γ k H) -> Γ' ⊢(Sc) -> Γ ⊢(Sc) t : s -> Γ' ⊢(Sc) t : s. +Proof. + intros H pr. induction 1. + - constructor. assumption. + - econstructor; swap 1 2. { apply H. } constructor. assumption. + - econstructor; try eassumption; auto. + apply IHtyping2. + + intros. simpl. destruct (lt_dec k n); try solve [constructor]. + apply ren_preserves_step_equiv. auto. + + econstructor; try eassumption. + apply IHtyping1; assumption. + - econstructor; try eassumption; auto. + + apply IHtyping2. + * intros. simpl. destruct (lt_dec k n); try solve [constructor]. + apply ren_preserves_step_equiv. auto. + * econstructor; try eassumption. + apply IHtyping1; assumption. + + apply IHtyping3. + * intros. simpl. destruct (lt_dec k n); try solve [constructor]. + apply ren_preserves_step_equiv. auto. + * econstructor; try assumption. apply IHtyping1; assumption. + - econstructor; auto. + - econstructor; eauto. +Qed. + +Lemma weakening {Sc n k} {σ: {i | i < n} -> {i | i < k}} {Γ Γ' x T} : + (forall i, + ren σ (kth_index_ctx Γ (proj1_sig i) (proj2_sig i)) = + kth_index_ctx Γ' (proj1_sig (σ i)) (proj2_sig (σ i))) -> + Γ ⊢(Sc) x : T -> Γ' ⊢(Sc) -> Γ' ⊢(Sc) ren σ x : ren σ T. + intro H. induction 1 in k, σ, Γ', H |- *; simpl; intro. + - constructor. assumption. + - rewrite H. constructor. assumption. + - econstructor; try eassumption. + + apply IHtyping1; try assumption. + + apply IHtyping2; try assumption. + * intro. unfold lift at 2 3. destruct (lt_dec (proj1_sig i) n); simpl. + -- rewrite ren_comp. destruct (lt_dec _ _); try tauto. + epose proof (proj2_sig (σ (exist _ (proj1_sig i) l))). simpl in *. + destruct (lt_dec _ _); try tauto. + replace l1 with (proj2_sig (σ (exist _ (proj1_sig i) l))) by apply le_unique. + rewrite <- H. rewrite ren_comp. simpl. replace l with l0 by apply le_unique. + apply ren_ext, lift_weaken. + -- destruct (lt_dec _ _); try tauto. rewrite ren_comp. destruct (lt_dec _ _); try lia. + rewrite ren_comp. apply ren_ext, lift_weaken. + * econstructor; try assumption. apply IHtyping1; assumption. + - econstructor; try eassumption. + + apply IHtyping1; assumption. + + apply IHtyping2. + * intro. unfold lift at 2 3. destruct (lt_dec (proj1_sig i) n); simpl. + -- rewrite ren_comp. destruct (lt_dec _ _); try tauto. + epose proof (proj2_sig (σ (exist _ (proj1_sig i) l))). simpl in *. + destruct (lt_dec _ _); try tauto. + replace l1 with (proj2_sig (σ (exist _ (proj1_sig i) l))) by apply le_unique. + rewrite <- H. rewrite ren_comp. simpl. replace l with l0 by apply le_unique. + apply ren_ext, lift_weaken. + -- destruct (lt_dec _ _); try tauto. rewrite ren_comp. destruct (lt_dec _ _); try lia. + rewrite ren_comp. apply ren_ext, lift_weaken. + * econstructor; eauto. + + apply IHtyping3. + * intro. unfold lift at 2 3. destruct (lt_dec (proj1_sig i) n); simpl. + -- rewrite ren_comp. destruct (lt_dec _ _); try tauto. + epose proof (proj2_sig (σ (exist _ (proj1_sig i) l))). simpl in *. + destruct (lt_dec _ _); try tauto. + replace l1 with (proj2_sig (σ (exist _ (proj1_sig i) l))) by apply le_unique. + rewrite <- H. rewrite ren_comp. simpl. replace l with l0 by apply le_unique. + apply ren_ext, lift_weaken. + -- destruct (lt_dec _ _); try tauto. rewrite ren_comp. destruct (lt_dec _ _); try lia. + rewrite ren_comp. apply ren_ext, lift_weaken. + * econstructor; eauto. + - simpl in *. rewrite ren_bind. + replace (bind (ren σ ∘ bind_first u) B) with (bind (bind_first (ren σ u)) (ren (lift σ) B)). + + econstructor; eauto. + + rewrite bind_ren. apply bind_ext. intro. unfold lift, bind_first. simpl. + destruct (lt_dec _ n). + * simpl. pose proof (proj2_sig (σ (exist _ (proj1_sig i) l))). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + * simpl. destruct (lt_dec _ _); try lia. reflexivity. + - econstructor. + + apply IHtyping; assumption. + + apply ren_preserves_step_equiv. assumption. +Qed. + +Lemma preservation (Sc: pi_scheme) {n} Γ (t u : term n) A : + Γ ⊢(Sc) t : A -> t ≻ u -> Γ ⊢(Sc) u : A. +Proof. + induction 1; intro red; inversion red; clear red; + match goal with H : fill ?K _ = _ _ |- _ => (destruct K; simpl in *; try discriminate; + subst; try solve [ match goal with H : _ [≻] _ |- _ => inversion H end ]) | _ => idtac end. + - inversion H2; subst; clear H2. econstructor; try eassumption. + + apply IHtyping1. constructor. assumption. + + eapply equiv_context; try eassumption. + * simpl. intros. destruct (lt_dec _ _); try solve [constructor]. + apply ren_preserves_step_equiv. apply Requiv_clot_r. constructor. assumption. + * econstructor; try eauto. { eapply typing_imp_ctx_wf. eassumption. } apply IHtyping1. + constructor. assumption. + - inversion H2; subst; clear H2. econstructor; try eassumption. + apply IHtyping2. constructor. assumption. + - inversion H3; subst; clear H3. unshelve econstructor. { exact (Pi (fill K u0) B). } + + econstructor; try eauto. + * apply IHtyping1. constructor. assumption. + * eapply equiv_context; try eassumption. + -- simpl. intros. destruct (lt_dec _ _); try solve [constructor]. + apply ren_preserves_step_equiv, Requiv_clot_r. constructor. assumption. + -- econstructor. + ++ eapply typing_imp_ctx_wf; eassumption. + ++ apply IHtyping1. constructor. assumption. + * eapply equiv_context; try eassumption. + -- simpl. intros. destruct (lt_dec _ _); try solve [constructor]. + apply ren_preserves_step_equiv, Requiv_clot_r. constructor. assumption. + -- econstructor. + ++ eapply typing_imp_ctx_wf; eassumption. + ++ apply IHtyping1. constructor. assumption. + + apply Requiv_clot_r. change (Pi (fill K ?x) B) with (fill (PiL K B) x). constructor. + assumption. + - inversion H3; subst; clear H3. econstructor; try eassumption. + apply IHtyping3. constructor. assumption. + - inversion H2; subst; clear H2. clear IHtyping1 IHtyping2. + rename u0 into u. + apply typ_abs_inv in H. destruct H as [s [s' [B0 H]]]. + destruct H as [Hequiv [type_ty [type_B0 [type_body pi_check]]]]. + apply pi_equiv_pi in Hequiv as [Aequiv Bequiv]. + assert (true_type_body : Γ, ty ⊢(Sc) body : B). + { econstructor; eauto using Requiv_sym. } + assert (true_type_u : Γ ⊢(Sc) u : ty). + { econstructor; eauto. } + revert true_type_body true_type_u. clear. intros tybody tyu. + enough ( + forall n k (σ : {i | i < k} -> term n) Γ Γ' x T, + (forall i, Γ ⊢(Sc) σ i : bind σ (kth_index_ctx Γ' (proj1_sig i) (proj2_sig i))) -> + Γ' ⊢(Sc) x : T -> Γ ⊢(Sc) -> Γ ⊢(Sc) bind σ x : bind σ T). + { eapply H; eauto using typing_imp_ctx_wf. + intro. destruct i; simpl. unfold bind_first at 1. simpl. destruct (lt_dec _ _). + - rewrite bind_ren. rewrite bind_id. + + constructor. eapply typing_imp_ctx_wf; eassumption. + + unfold bind_first, weaken. simpl. intro. pose proof (proj2_sig k). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + - rewrite bind_ren. rewrite bind_id; try assumption. + unfold bind_first, weaken. simpl. intro. pose proof (proj2_sig k). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + } + clear. intros ? ? ? ? ? ? ? H tyx Γwf. induction tyx in n, σ, Γ, H, Γwf |- *; simpl in *; auto. + + constructor. assumption. + + econstructor; eauto. eapply IHtyx2. + * intro. unfold lift_bind at 1. destruct (lt_dec _ _). + -- rewrite bind_weaken. eapply weakening. + ++ intro. simpl. pose proof (proj2_sig i0). destruct (lt_dec _ _); try tauto. + f_equal. f_equal. apply le_unique. + ++ apply H. + ++ econstructor; eauto. + -- rewrite bind_weaken. + replace (ren weaken (bind σ A)) with + (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). + ++ constructor. econstructor; eauto. + ++ simpl. destruct (lt_dec n n); try lia. reflexivity. + * econstructor; eauto. + + econstructor; eauto. + * apply IHtyx2. + -- intro. rewrite bind_weaken. unfold lift_bind. + destruct (lt_dec _ _). + ++ eapply weakening; eauto. + ** intro. simpl. pose proof (proj2_sig i0). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. f_equal. apply le_unique. + ** econstructor; eauto. + ++ replace (ren weaken (bind σ A)) with + (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). + ** do 2 econstructor; eauto. + ** simpl. destruct (lt_dec _ _); try lia. reflexivity. + -- econstructor; eauto. + * apply IHtyx3. + -- intro. rewrite bind_weaken. unfold lift_bind at 1. destruct (lt_dec _ _). + ++ eapply weakening; eauto. + ** intro. simpl. pose proof (proj2_sig i0). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. f_equal. apply le_unique. + ** econstructor; eauto. + ++ replace (ren weaken (bind σ A)) with + (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). + ** do 2 econstructor; eauto. + ** simpl. destruct (lt_dec _ _); try lia. reflexivity. + -- econstructor; eauto. + + rewrite bind_comp. replace (bind (bind σ ∘ bind_first u) B) with + (bind (bind_first (bind σ u)) (bind (lift_bind σ) B)). + * econstructor; eauto. + * rewrite bind_comp. apply bind_ext. intro. unfold lift_bind, bind_first at 2. + destruct (lt_dec _ _); simpl. + -- rewrite bind_ren. apply bind_id. intro. unfold weaken, bind_first. simpl. + pose proof (proj2_sig k). simpl in *. destruct (lt_dec _ _); try tauto. + f_equal. apply sig_lt_ext. reflexivity. + -- unfold bind_first. simpl. destruct (lt_dec _ _); try lia. reflexivity. + + econstructor; eauto. apply bind_preserves_step_equiv. assumption. + - inversion H1; subst; clear H1. econstructor; try eassumption. + apply IHtyping1. constructor. assumption. + - inversion H1; subst; clear H1. econstructor. + + econstructor; try eassumption. apply IHtyping2. constructor. assumption. + + apply bind_preserves_step_equiv_in_subs. intro. unfold bind_first. + destruct (lt_dec _ _). + * constructor. + * apply Requiv_clot_r. constructor. assumption. + - subst. econstructor; try eassumption. apply IHtyping. constructor. assumption. +Qed. From 12f7e8f1af44fc0a140ef198515720c53e4ad299 Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Tue, 18 Nov 2025 23:13:17 +0100 Subject: [PATCH 15/21] proved subject reduction (last time it was only preservation) --- theories/LambdaCube/Typing.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/theories/LambdaCube/Typing.v b/theories/LambdaCube/Typing.v index 347aac3..aaf56bf 100644 --- a/theories/LambdaCube/Typing.v +++ b/theories/LambdaCube/Typing.v @@ -357,3 +357,10 @@ Proof. * apply Requiv_clot_r. constructor. assumption. - subst. econstructor; try eassumption. apply IHtyping. constructor. assumption. Qed. + +Lemma subject_reduction (Sc: pi_scheme) {n} Γ (t u : term n) A : + Γ ⊢(Sc) t : A -> t ≻* u -> Γ ⊢(Sc) u : A. +Proof. + destruct 2; auto. + induction H0; eapply preservation; eauto. +Qed. From f7e3f17a9bd117ef210baeaf4457bca7d31ad368 Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Wed, 19 Nov 2025 12:49:09 +0100 Subject: [PATCH 16/21] fixed naming conflict that appeared when merging --- theories/LambdaCube/Typing.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/LambdaCube/Typing.v b/theories/LambdaCube/Typing.v index aaf56bf..418ac8e 100644 --- a/theories/LambdaCube/Typing.v +++ b/theories/LambdaCube/Typing.v @@ -292,10 +292,10 @@ Proof. intro. destruct i; simpl. unfold bind_first at 1. simpl. destruct (lt_dec _ _). - rewrite bind_ren. rewrite bind_id. + constructor. eapply typing_imp_ctx_wf; eassumption. - + unfold bind_first, weaken. simpl. intro. pose proof (proj2_sig k). simpl in *. + + unfold bind_first, weaken. simpl. intro i. pose proof (proj2_sig i). simpl in *. destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. - rewrite bind_ren. rewrite bind_id; try assumption. - unfold bind_first, weaken. simpl. intro. pose proof (proj2_sig k). simpl in *. + unfold bind_first, weaken. simpl. intro i. pose proof (proj2_sig i). simpl in *. destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. } clear. intros ? ? ? ? ? ? ? H tyx Γwf. induction tyx in n, σ, Γ, H, Γwf |- *; simpl in *; auto. From b43ec19ee68b19bdd55ad95d098369a1a8005b97 Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Thu, 20 Nov 2025 18:08:31 +0100 Subject: [PATCH 17/21] fixed typing! When converting types, we ask the 2 types to be convertible --- theories/LambdaCube/Operational.v | 99 ++++++++ theories/LambdaCube/Typing.v | 374 +++++++++++++++++++++--------- 2 files changed, 362 insertions(+), 111 deletions(-) diff --git a/theories/LambdaCube/Operational.v b/theories/LambdaCube/Operational.v index ade16c2..f21536c 100644 --- a/theories/LambdaCube/Operational.v +++ b/theories/LambdaCube/Operational.v @@ -508,6 +508,105 @@ Proof. intro H. apply srt_equiv in H. apply srt_star in H. congruence. Qed. +Lemma no_spontaneous_srt_ren {k n m s} {σ: {i | i < k} -> {i | i < n}} {t : term k} {K: ctx m n} : + ren σ t = fill K (Srt s) -> exists k0 (K' : ctx k0 k), t = fill K' (Srt s). + induction t in n, m, σ, K |- *; simpl; destruct K; intro e; inversion e; clear e; subst. + - apply IHt1 in H0 as [k [K' e]]. subst. exists _, (PiL K' t2). reflexivity. + - apply IHt2 in H1 as [k [K' e]]. subst. exists _, (PiR t1 K'). reflexivity. + - apply IHt1 in H0 as [k [K' e]]. subst. exists _, (AbsL K' t2). reflexivity. + - apply IHt2 in H1 as [k [K' e]]. subst. exists _, (AbsR t1 K'). reflexivity. + - apply IHt1 in H0 as [k [K' e]]. subst. exists _, (AppL K' t2). reflexivity. + - apply IHt2 in H1 as [k [K' e]]. subst. exists _, (AppR t1 K'). reflexivity. + - exists _, Hole. reflexivity. +Qed. + +Lemma no_spontaneous_srt_bind {k n m s} {σ: {i | i < k} -> term n} {t : term k} {K: ctx m n} : + bind σ t = fill K (Srt s) -> + (exists k0 (K': ctx k0 k), t = fill K' (Srt s)) \/ (exists i k0 (K': ctx k0 n), σ i = fill K' (Srt s)). + induction t in n, m, σ, K |- *; simpl. + - right. repeat eexists; eassumption. + - destruct K; simpl; intro H; inversion H; subst; clear H. + + apply IHt1 in H1. destruct H1 as [[k [K' e]]| [i [k [K' e]]]]. + * subst. left. eexists. exists (PiL K' t2). reflexivity. + * right. repeat eexists; eassumption. + + apply IHt2 in H2. destruct H2 as [[k [K' e]]| [i [k [K' e]]]]. + * subst. left. eexists. exists (PiR t1 K'). reflexivity. + * right. unfold lift_bind in *. destruct (lt_dec _ _); swap 1 2. + { exfalso. revert e. clear. remember (exist _ _ _) eqn: e. clear e. + destruct K'; discriminate. } + apply no_spontaneous_srt_ren in e as [k0 [K0 e]]. repeat eexists; eassumption. + - destruct K; simpl; intro H; inversion H; subst; clear H. + + apply IHt1 in H1. destruct H1 as [[k [K' e]]| [i [k [K' e]]]]. + * subst. left. eexists. exists (AbsL K' t2). reflexivity. + * right. repeat eexists; eassumption. + + apply IHt2 in H2. destruct H2 as [[k [K' e]]| [i [k [K' e]]]]. + * subst. left. eexists. exists (AbsR t1 K'). reflexivity. + * right. unfold lift_bind in *. destruct (lt_dec _ _); swap 1 2. + { exfalso. revert e. clear. remember (exist _ _ _) eqn: e. clear e. + destruct K'; discriminate. } + apply no_spontaneous_srt_ren in e as [k0 [K0 e]]. repeat eexists; eassumption. + - destruct K; simpl; intro H; inversion H; subst; clear H. + + apply IHt1 in H1. destruct H1 as [[k [K' e]]| [i [k [K' e]]]]. + * subst. left. eexists. exists (AppL K' t2). reflexivity. + * right. repeat eexists; eassumption. + + apply IHt2 in H2. destruct H2 as [[k [K' e]]| [i [k [K' e]]]]. + * subst. left. eexists. exists (AppR t1 K'). reflexivity. + * right. repeat eexists; eassumption. + - destruct K; simpl; intro e; inversion e; subst; clear e. left. exists _, Hole. reflexivity. +Qed. + +Lemma no_spontaneous_srt_redex {k n} {s t} {K: ctx k n} : + t [≻] fill K (Srt s) -> exists k0 (K': ctx k0 n), t = fill K' (Srt s). +Proof. + inversion 1; subst; clear H. + apply no_spontaneous_srt_bind in H2 as [[m [K' e]] | [i [m [K' e]]]]. + - subst. eexists. exists (AppL (AbsR ty K') arg). reflexivity. + - unfold bind_first in *. destruct (lt_dec _ _). { destruct K'; try discriminate. } subst. + eexists _, (AppR _ K'). simpl. reflexivity. +Qed. + +Lemma no_spontaneous_srt_step {k n} {s t} {K: ctx k n} : + t ≻ fill K (Srt s) -> exists k0 (K': ctx k0 n), t = fill K' (Srt s). +Proof. + intro r. inversion r; subst; clear r. induction K0; simpl in *. + - subst. eapply no_spontaneous_srt_redex. eassumption. + - destruct K; simpl in *; inversion H; subst; clear H. + + apply IHK0 in H2 as [m [K' e]]. rewrite e. exists _, (PiL K' t1). reflexivity. + + eexists _, (PiR _ K). reflexivity. + - destruct K; simpl in *; inversion H; subst; clear H. + + apply IHK0 in H2 as [m [K' e]]. rewrite e. exists _, (AbsL K' t1). reflexivity. + + eexists _, (AbsR _ K). reflexivity. + - destruct K; simpl in *; inversion H; subst; clear H. + + apply IHK0 in H2 as [m [K' e]]. rewrite e. exists _, (AppL K' t1). reflexivity. + + eexists _, (AppR _ K). reflexivity. + - destruct K; simpl in *; inversion H; subst; clear H. + + eexists _, (PiL K _). reflexivity. + + apply IHK0 in H3 as [m [K' e]]. rewrite e. exists _, (PiR t1 K'). reflexivity. + - destruct K; simpl in *; inversion H; subst; clear H. + + eexists _, (AbsL K _). reflexivity. + + apply IHK0 in H3 as [m [K' e]]. rewrite e. exists _, (AbsR t1 K'). reflexivity. + - destruct K; simpl in *; inversion H; subst; clear H. + + eexists _, (AppL K _). reflexivity. + + apply IHK0 in H3 as [m [K' e]]. rewrite e. exists _, (AppR t1 K'). reflexivity. +Qed. + +Lemma no_spontaneous_srt_step_plus {k n} {s t} {K: ctx k n} : + t ≻+ fill K (Srt s) -> exists k0 (K': ctx k0 n), t = fill K' (Srt s). +Proof. + remember (fill K (Srt s)). + induction 1 in k, K, s, Heqt0 |- *; subst. + - apply no_spontaneous_srt_step in H0 as [k' [K' e]]. apply IHRplus in e. firstorder. + - apply no_spontaneous_srt_step in H as [k' [K' e]]. firstorder. +Qed. + +Lemma no_spontaneous_srt_step_star {k n} {s t} {K: ctx k n} : + t ≻* fill K (Srt s) -> exists k0 (K': ctx k0 n), t = fill K' (Srt s). +Proof. + remember (fill _ _). destruct 1. + - subst. repeat eexists. + - subst. eapply no_spontaneous_srt_step_plus. eassumption. +Qed. + Lemma no_var_step {n} {i} {t: term n} : ¬ (Var i ≻ t). Proof. inversion 1; subst; clear H. destruct K; try discriminate. simpl in *. subst. inversion H1. diff --git a/theories/LambdaCube/Typing.v b/theories/LambdaCube/Typing.v index 418ac8e..44b3e5d 100644 --- a/theories/LambdaCube/Typing.v +++ b/theories/LambdaCube/Typing.v @@ -46,8 +46,8 @@ Inductive typing (P: pi_scheme) : forall {n}, typing_ctx n -> term n -> term n - Γ ⊢(P) Abs A t : Pi A B | typ_app {n} {Γ: typing_ctx n} {A B t u} : Γ ⊢(P) t : Pi A B -> Γ ⊢(P) u : A -> Γ ⊢(P) App t u : bind (bind_first u) B -| typ_conv {n} {Γ: typing_ctx n} {t A B} : - Γ ⊢(P) t : A -> A ≅ B -> Γ ⊢(P) t : B +| typ_conv {n} {Γ: typing_ctx n} {t A B s} : + Γ ⊢(P) t : A -> A ≅ B -> Γ ⊢(P) B : Srt s -> Γ ⊢(P) t : B with ctx_wf (P: pi_scheme) : forall {n}, typing_ctx n -> Prop := | empty_wf : \ ⊢(P) | cons_wf {n} {A: typing_ctx n} {t: term n} {s} : @@ -112,7 +112,7 @@ Lemma typ_var_inv Sc {n} (Γ : typing_ctx n) i T : (Γ ⊢(Sc) Var i : T) -> T ≅ kth_index_ctx Γ (proj1_sig i) (proj2_sig i). remember (Var i). induction 1 in i, Heqt |- *; try discriminate. - inversion Heqt. subst. constructor. - - subst. specialize (IHtyping _ eq_refl). eapply Requiv_trans; eauto using Requiv_sym. + - subst. specialize (IHtyping1 _ eq_refl). eapply Requiv_trans; eauto using Requiv_sym. Qed. Lemma typ_pi_inv Sc {n} (Γ : typing_ctx n) A B T : @@ -121,23 +121,23 @@ Lemma typ_pi_inv Sc {n} (Γ : typing_ctx n) A B T : Proof. remember (Pi A B). induction 1 in A, B, Heqt |- *; try discriminate. - exists s. exists s'. inversion Heqt; subst; clear Heqt. intuition constructor. - - subst. specialize (IHtyping _ _ eq_refl). destruct IHtyping as [s [s']]. - exists s. exists s'. intuition. eauto using Requiv_trans, Requiv_sym. + - subst. specialize (IHtyping1 _ _ eq_refl). destruct IHtyping1 as [s0 [s']]. + exists s0. exists s'. intuition. eauto using Requiv_trans, Requiv_sym. Qed. Lemma typ_abs_inv Sc {n} (Γ: typing_ctx n) A t T : Γ ⊢(Sc) Abs A t : T -> - exists s s' B, + exists s s' B X, T ≅ Pi A B /\ Γ ⊢(Sc) A : Srt s /\ Γ, A ⊢(Sc) B : Srt s' /\ Γ, A ⊢(Sc) t : B /\ - pi_scheme_check Sc s s'. + Γ ⊢(Sc) T : X /\ pi_scheme_check Sc s s'. Proof. remember (Abs A t). induction 1 in A, t, Heqt0 |- *; try discriminate. - clear IHtyping1 IHtyping2 IHtyping3. inversion Heqt0. subst. clear Heqt0. - exists s. exists s'. exists B. intuition constructor. - - subst. specialize (IHtyping A t eq_refl). - destruct IHtyping as [s [s' [B0]]]. - exists s. exists s'. exists B0. intuition eauto using Requiv_trans, Requiv_sym. + exists s. exists s'. exists B. exists (Srt s'). intuition econstructor; eassumption. + - subst. specialize (IHtyping1 A t eq_refl). + destruct IHtyping1 as [s0 [s' [B0]]]. + exists s0, s', B0, (Srt s). firstorder eauto using Requiv_trans, Requiv_sym. Qed. Lemma typ_app_inv Sc {n} (Γ: typing_ctx n) t u T : @@ -146,8 +146,8 @@ Proof. remember (App t u) as t0. induction 1 in t, u, Heqt0 |- *; try discriminate. - clear IHtyping1 IHtyping2. exists A, B. inversion Heqt0; subst; clear Heqt0. intuition constructor. - - subst. specialize (IHtyping _ _ eq_refl). - destruct IHtyping as [A0 [B0]]. + - subst. specialize (IHtyping1 _ _ eq_refl). + destruct IHtyping1 as [A0 [B0]]. exists A0, B0. intuition eauto using Requiv_trans, Requiv_sym. Qed. @@ -156,33 +156,7 @@ Proof. induction 1; try assumption. Qed. -Lemma equiv_context (Sc : pi_scheme) {n} (Γ Γ': typing_ctx n) t s : - (forall k H, kth_index_ctx Γ' k H ≅ kth_index_ctx Γ k H) -> Γ' ⊢(Sc) -> Γ ⊢(Sc) t : s -> Γ' ⊢(Sc) t : s. -Proof. - intros H pr. induction 1. - - constructor. assumption. - - econstructor; swap 1 2. { apply H. } constructor. assumption. - - econstructor; try eassumption; auto. - apply IHtyping2. - + intros. simpl. destruct (lt_dec k n); try solve [constructor]. - apply ren_preserves_step_equiv. auto. - + econstructor; try eassumption. - apply IHtyping1; assumption. - - econstructor; try eassumption; auto. - + apply IHtyping2. - * intros. simpl. destruct (lt_dec k n); try solve [constructor]. - apply ren_preserves_step_equiv. auto. - * econstructor; try eassumption. - apply IHtyping1; assumption. - + apply IHtyping3. - * intros. simpl. destruct (lt_dec k n); try solve [constructor]. - apply ren_preserves_step_equiv. auto. - * econstructor; try assumption. apply IHtyping1; assumption. - - econstructor; auto. - - econstructor; eauto. -Qed. - -Lemma weakening {Sc n k} {σ: {i | i < n} -> {i | i < k}} {Γ Γ' x T} : +Lemma gen_weakening {Sc n k} {σ: {i | i < n} -> {i | i < k}} {Γ Γ' x T} : (forall i, ren σ (kth_index_ctx Γ (proj1_sig i) (proj2_sig i)) = kth_index_ctx Γ' (proj1_sig (σ i)) (proj2_sig (σ i))) -> @@ -236,126 +210,304 @@ Lemma weakening {Sc n k} {σ: {i | i < n} -> {i | i < k}} {Γ Γ' x T} : destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. * simpl. destruct (lt_dec _ _); try lia. reflexivity. - econstructor. - + apply IHtyping; assumption. + + apply IHtyping1; assumption. + apply ren_preserves_step_equiv. assumption. + + apply IHtyping2; assumption. +Qed. + +Lemma weakening {Sc n} {Γ: typing_ctx n} {A x T s}: + Γ ⊢(Sc) x : T -> Γ ⊢(Sc) A : Srt s -> Γ, A ⊢(Sc) ren weaken x : ren weaken T. +Proof. + intros. eapply gen_weakening; eauto. + - destruct i; simpl. destruct (lt_dec _ _); try tauto. f_equal. f_equal. apply le_unique. + - econstructor; try eassumption. eapply typing_imp_ctx_wf; eassumption. +Qed. + +Lemma wf_ctx_contains_types {Sc n} {Γ : typing_ctx n} {k l} : + Γ ⊢(Sc) -> exists s, Γ ⊢(Sc) kth_index_ctx Γ k l : Srt s. + induction 1 in k, l |- *; simpl. + - destruct (Nat.nlt_0_r _ _). + - destruct (lt_dec _ _). + + edestruct IHctx_wf as [s']. change (Srt ?s) with (ren (@weaken n) (Srt s)). + eexists. eapply weakening; eassumption. + + exists s. change (Srt s) with (ren (@weaken n) (Srt s)). eapply weakening; eassumption. +Qed. + +Lemma equiv_context (Sc : pi_scheme) {n} (Γ Γ': typing_ctx n) t s : + (forall k H, kth_index_ctx Γ' k H ≅ kth_index_ctx Γ k H) -> + (forall k H, exists s, Γ' ⊢(Sc) kth_index_ctx Γ k H : Srt s) -> + Γ' ⊢(Sc) -> Γ ⊢(Sc) t : s -> Γ' ⊢(Sc) t : s. +Proof. + intros H Htyp pr. induction 1. + - constructor. assumption. + - edestruct Htyp. econstructor; swap 1 2; try eassumption. + + apply H. + + constructor. assumption. + - econstructor; try eassumption; auto. + apply IHtyping2. + + intros. simpl. destruct (lt_dec k n); try solve [constructor]. + apply ren_preserves_step_equiv. auto. + + simpl. intros. destruct (lt_dec _ _). + * edestruct Htyp as [s0]. exists s0. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; eauto. + * exists s. change (@Srt (S n) s) with (ren weaken (@Srt n s)). eapply weakening; eauto. + + econstructor; try eassumption. + apply IHtyping1; assumption. + - econstructor; try eassumption; auto. + + apply IHtyping2. + * intros. simpl. destruct (lt_dec k n); try solve [constructor]. + apply ren_preserves_step_equiv. auto. + * intros. simpl. destruct (lt_dec _ _). + -- edestruct Htyp as [s0]. exists s0. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; try eassumption. + apply IHtyping1; assumption. + -- exists s. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; apply IHtyping1; assumption. + * econstructor; try eassumption. + apply IHtyping1; assumption. + + apply IHtyping3. + * intros. simpl. destruct (lt_dec k n); try solve [constructor]. + apply ren_preserves_step_equiv. auto. + * intros. simpl. destruct (lt_dec _ _). + -- edestruct Htyp as [s0]. exists s0. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; try eassumption. + apply IHtyping1; assumption. + -- exists s. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; apply IHtyping1; assumption. + * econstructor; try assumption. apply IHtyping1; assumption. + - econstructor; auto. + - econstructor; eauto. +Qed. + +Lemma bind_typ Sc n k (σ : {i | i < k} -> term n) Γ Γ' x T : + (forall i, Γ ⊢(Sc) σ i : bind σ (kth_index_ctx Γ' (proj1_sig i) (proj2_sig i))) -> + Γ' ⊢(Sc) x : T -> Γ ⊢(Sc) -> Γ ⊢(Sc) bind σ x : bind σ T. + intros H tyx Γwf. induction tyx in n, σ, Γ, H, Γwf |- *; simpl in *; auto. + - constructor. assumption. + - econstructor; eauto. eapply IHtyx2. + + intro. unfold lift_bind at 1. destruct (lt_dec _ _). + * rewrite bind_weaken. eapply weakening; eauto. + * rewrite bind_weaken. + replace (ren weaken (bind σ A)) with + (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). + -- constructor. econstructor; eauto. + -- simpl. destruct (lt_dec n n); try lia. reflexivity. + + econstructor; eauto. + - econstructor; eauto. + + apply IHtyx2. + * intro. rewrite bind_weaken. unfold lift_bind. + destruct (lt_dec _ _). + -- eapply weakening; eauto. + -- replace (ren weaken (bind σ A)) with + (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). + ++ do 2 econstructor; eauto. + ++ simpl. destruct (lt_dec _ _); try lia. reflexivity. + * econstructor; eauto. + + apply IHtyx3. + * intro. rewrite bind_weaken. unfold lift_bind at 1. destruct (lt_dec _ _). + -- eapply weakening; eauto. + -- replace (ren weaken (bind σ A)) with + (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). + ++ do 2 econstructor; eauto. + ++ simpl. destruct (lt_dec _ _); try lia. reflexivity. + * econstructor; eauto. + - rewrite bind_comp. replace (bind (bind σ ∘ bind_first u) B) with + (bind (bind_first (bind σ u)) (bind (lift_bind σ) B)). + + econstructor; eauto. + + rewrite bind_comp. apply bind_ext. intro. unfold lift_bind, bind_first at 2. + destruct (lt_dec _ _); simpl. + * rewrite bind_ren. apply bind_id. intro. unfold weaken, bind_first. simpl. + pose proof (proj2_sig k). simpl in *. destruct (lt_dec _ _); try tauto. + f_equal. apply sig_lt_ext. reflexivity. + * unfold bind_first. simpl. destruct (lt_dec _ _); try lia. reflexivity. + - econstructor; eauto. apply bind_preserves_step_equiv. assumption. +Qed. + +Lemma typed_imp_subterm_typed {Sc} {n k} {Γ u T} {K: ctx k n} : + Γ ⊢(Sc) fill K u : T -> exists Γ' T', Γ' ⊢(Sc) u : T'. + remember (fill K u) as t. induction 1 in k, u, K, Heqt |- *. + - destruct K; simpl in *; try discriminate. subst. + do 2 eexists. constructor. eassumption. + - destruct K; simpl in *; try discriminate. subst. do 2 eexists. constructor. eassumption. + - destruct K; simpl in *; try discriminate. + + subst. do 2 eexists. econstructor; eassumption. + + inversion Heqt. eauto. + + inversion Heqt. eauto. + - destruct K; simpl in *; try discriminate. + + subst. do 2 eexists. econstructor; eassumption. + + inversion Heqt. eauto. + + inversion Heqt. eauto. + - destruct K; simpl in *; try discriminate. + + subst. do 2 eexists. econstructor; eassumption. + + inversion Heqt. eauto. + + inversion Heqt. eauto. + - eauto. +Qed. + +Lemma unique_typing {n Sc Γ} {t A B: term n} : + Γ ⊢(Sc) t : A -> Γ ⊢(Sc) t : B -> A ≅ B. +Proof. + induction 1 in B |- *. + - intro H'. apply typ_star_inv in H'. apply Requiv_sym. assumption. + - intro H'. apply typ_var_inv in H'. apply Requiv_sym. assumption. + - intro H'. apply typ_pi_inv in H' as [s0 [s'0 [Bequiv [typA [typB0 pi_check']]]]]. + specialize (IHtyping2 _ typB0). apply srt_equiv_srt in IHtyping2. subst. + apply Requiv_sym. assumption. + - intro H'. apply typ_abs_inv in H' as [s0 [s0' [B' [S [Bequiv H']]]]]. + apply Requiv_sym. eapply Requiv_trans; try eassumption. + change (Pi A ?x) with (fill (PiR A Hole) x). + apply step_equiv_context. apply Requiv_sym. intuition eauto. + - intro H'. apply typ_app_inv in H' as [A' [B' [Bequiv H']]]. + refine (Requiv_trans _ (Requiv_sym _)); try eassumption. apply bind_preserves_step_equiv. + destruct H' as [typA _]. apply IHtyping1 in typA. apply pi_equiv_pi in typA. tauto. + - intro. eauto using Requiv_trans, Requiv_sym. +Qed. + +Lemma srt_typing {n Sc} {Γ t} {T: term n} : + Γ ⊢(Sc) t : T -> T = Srt Box \/ (exists s, Γ ⊢(Sc) T: Srt s). +Proof. + induction 1; auto. + - right. induction H; simpl. + + destruct (Nat.nlt_0_r _ _). + + destruct (lt_dec _ _). + * destruct (IHctx_wf (exist _ (proj1_sig i) l)) as [s']. + exists s'. change (Srt s') with (@ren n _ weaken (Srt s')). eapply weakening; try eassumption. + * exists s. change (Srt s) with (@ren n _ weaken (Srt s)). eapply weakening; try eassumption. + - destruct s'. + + right. exists Box. constructor. eapply typing_imp_ctx_wf. eassumption. + + left. constructor. + - right. exists s'. econstructor; try eassumption. + - destruct IHtyping1 as [|[s IHtyping1]]; try discriminate. + right. exists s. + apply typ_pi_inv in IHtyping1 as [s' [s'' [equiv_srts [typA [typB Sc_check]]]]]. + apply srt_equiv_srt in equiv_srts. subst. rename s' into s, s'' into s'. + change (Srt s') with (bind (bind_first u) (Srt s')). + eapply bind_typ; try eassumption. + * intro. unfold bind_first at 1. simpl. rewrite bind_ren. rewrite bind_id. + { destruct (lt_dec _ _); try assumption. constructor. eauto using typing_imp_ctx_wf. } + clear. destruct k. unfold bind_first. simpl. destruct (lt_dec x n); try tauto. + f_equal. apply sig_lt_ext. reflexivity. + * eauto using typing_imp_ctx_wf. + - destruct IHtyping1. + + subst. apply srt_equiv in H0. left. clear IHtyping2. clear dependent t. + apply @no_spontaneous_srt_step_star with (K := Hole) in H0 as [k [K e]]. subst. + apply typed_imp_subterm_typed in H1 as [Γ' [T H]]. exfalso. revert H. clear. + remember (Srt Box). induction 1 in Heqt |- *; try discriminate; tauto. + + right. eauto. Qed. Lemma preservation (Sc: pi_scheme) {n} Γ (t u : term n) A : Γ ⊢(Sc) t : A -> t ≻ u -> Γ ⊢(Sc) u : A. Proof. induction 1; intro red; inversion red; clear red; - match goal with H : fill ?K _ = _ _ |- _ => (destruct K; simpl in *; try discriminate; - subst; try solve [ match goal with H : _ [≻] _ |- _ => inversion H end ]) | _ => idtac end. + match goal with + | H : fill ?K _ = _ _ |- _ => + (destruct K; simpl in *; try discriminate; + subst; try solve [ match goal with H : _ [≻] _ |- _ => inversion H end ]) + | _ => idtac end. - inversion H2; subst; clear H2. econstructor; try eassumption. + apply IHtyping1. constructor. assumption. + eapply equiv_context; try eassumption. * simpl. intros. destruct (lt_dec _ _); try solve [constructor]. apply ren_preserves_step_equiv. apply Requiv_clot_r. constructor. assumption. + * intros. simpl. destruct (lt_dec _ _). + -- assert (wfΓ : Γ ⊢(Sc)) by eauto using typing_imp_ctx_wf. + epose proof (Htyp := wf_ctx_contains_types wfΓ). destruct Htyp as [s0]. + exists s0. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; eauto. apply IHtyping1. constructor. assumption. + -- exists s. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; eauto. apply IHtyping1. constructor. assumption. * econstructor; try eauto. { eapply typing_imp_ctx_wf. eassumption. } apply IHtyping1. constructor. assumption. - inversion H2; subst; clear H2. econstructor; try eassumption. apply IHtyping2. constructor. assumption. - - inversion H3; subst; clear H3. unshelve econstructor. { exact (Pi (fill K u0) B). } + - inversion H3; subst; clear H3. unshelve econstructor. + { exact (Pi (fill K u0) B). } + { exact s'. } + econstructor; try eauto. * apply IHtyping1. constructor. assumption. * eapply equiv_context; try eassumption. -- simpl. intros. destruct (lt_dec _ _); try solve [constructor]. apply ren_preserves_step_equiv, Requiv_clot_r. constructor. assumption. + -- simpl. intros. destruct (lt_dec _ _). + ++ assert (wfΓ : Γ ⊢(Sc)) by eauto using typing_imp_ctx_wf. + epose proof (Htyp := wf_ctx_contains_types wfΓ). destruct Htyp as [s0]. + exists s0. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; eauto. apply IHtyping1. constructor. assumption. + ++ exists s. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; eauto. apply IHtyping1. constructor. assumption. -- econstructor. ++ eapply typing_imp_ctx_wf; eassumption. ++ apply IHtyping1. constructor. assumption. * eapply equiv_context; try eassumption. -- simpl. intros. destruct (lt_dec _ _); try solve [constructor]. apply ren_preserves_step_equiv, Requiv_clot_r. constructor. assumption. + -- simpl. intros. destruct (lt_dec _ _). + ++ assert (wfΓ : Γ ⊢(Sc)) by eauto using typing_imp_ctx_wf. + epose proof (Htyp := wf_ctx_contains_types wfΓ). destruct Htyp as [s0]. + eexists. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; eauto. apply IHtyping1. constructor. assumption. + ++ eexists. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; eauto. apply IHtyping1. constructor. assumption. -- econstructor. ++ eapply typing_imp_ctx_wf; eassumption. ++ apply IHtyping1. constructor. assumption. + apply Requiv_clot_r. change (Pi (fill K ?x) B) with (fill (PiL K B) x). constructor. assumption. + + econstructor; eassumption. - inversion H3; subst; clear H3. econstructor; try eassumption. apply IHtyping3. constructor. assumption. - inversion H2; subst; clear H2. clear IHtyping1 IHtyping2. rename u0 into u. - apply typ_abs_inv in H. destruct H as [s [s' [B0 H]]]. - destruct H as [Hequiv [type_ty [type_B0 [type_body pi_check]]]]. + apply typ_abs_inv in H. destruct H as [s [s' [B0 [X H]]]]. + destruct H as [Hequiv [type_ty [type_B0 [type_body [typ_piAB pi_check]]]]]. apply pi_equiv_pi in Hequiv as [Aequiv Bequiv]. + apply typ_pi_inv in typ_piAB as [s0 [s0' [Xequiv [typA [typB pi_check2]]]]]. assert (true_type_body : Γ, ty ⊢(Sc) body : B). - { econstructor; eauto using Requiv_sym. } + { econstructor; eauto using Requiv_sym. eapply equiv_context; try eassumption. + - simpl. intros. apply ren_preserves_step_equiv. + destruct (lt_dec _ _); auto using Requiv_sym. constructor. + - simpl. intros. destruct (lt_dec k0 k). + + edestruct (@wf_ctx_contains_types); swap 1 2. + * eexists x. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; try eassumption. + * eapply typing_imp_ctx_wf. eassumption. + + exists s0. change (@Srt (S ?n) ?x) with (ren weaken (@Srt n x)). + eapply weakening; try eassumption. + - econstructor; try eassumption. eapply typing_imp_ctx_wf; eassumption. + } assert (true_type_u : Γ ⊢(Sc) u : ty). { econstructor; eauto. } revert true_type_body true_type_u. clear. intros tybody tyu. - enough ( - forall n k (σ : {i | i < k} -> term n) Γ Γ' x T, - (forall i, Γ ⊢(Sc) σ i : bind σ (kth_index_ctx Γ' (proj1_sig i) (proj2_sig i))) -> - Γ' ⊢(Sc) x : T -> Γ ⊢(Sc) -> Γ ⊢(Sc) bind σ x : bind σ T). - { eapply H; eauto using typing_imp_ctx_wf. - intro. destruct i; simpl. unfold bind_first at 1. simpl. destruct (lt_dec _ _). - - rewrite bind_ren. rewrite bind_id. - + constructor. eapply typing_imp_ctx_wf; eassumption. - + unfold bind_first, weaken. simpl. intro i. pose proof (proj2_sig i). simpl in *. - destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. - - rewrite bind_ren. rewrite bind_id; try assumption. - unfold bind_first, weaken. simpl. intro i. pose proof (proj2_sig i). simpl in *. + eapply bind_typ; eauto using typing_imp_ctx_wf. + intro. destruct i; simpl. unfold bind_first at 1. simpl. destruct (lt_dec _ _). + + rewrite bind_ren. rewrite bind_id. + * constructor. eapply typing_imp_ctx_wf; eassumption. + * unfold bind_first, weaken. simpl. intro i. pose proof (proj2_sig i). simpl in *. destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. - } - clear. intros ? ? ? ? ? ? ? H tyx Γwf. induction tyx in n, σ, Γ, H, Γwf |- *; simpl in *; auto. - + constructor. assumption. - + econstructor; eauto. eapply IHtyx2. - * intro. unfold lift_bind at 1. destruct (lt_dec _ _). - -- rewrite bind_weaken. eapply weakening. - ++ intro. simpl. pose proof (proj2_sig i0). destruct (lt_dec _ _); try tauto. - f_equal. f_equal. apply le_unique. - ++ apply H. - ++ econstructor; eauto. - -- rewrite bind_weaken. - replace (ren weaken (bind σ A)) with - (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). - ++ constructor. econstructor; eauto. - ++ simpl. destruct (lt_dec n n); try lia. reflexivity. - * econstructor; eauto. - + econstructor; eauto. - * apply IHtyx2. - -- intro. rewrite bind_weaken. unfold lift_bind. - destruct (lt_dec _ _). - ++ eapply weakening; eauto. - ** intro. simpl. pose proof (proj2_sig i0). simpl in *. - destruct (lt_dec _ _); try tauto. f_equal. f_equal. apply le_unique. - ** econstructor; eauto. - ++ replace (ren weaken (bind σ A)) with - (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). - ** do 2 econstructor; eauto. - ** simpl. destruct (lt_dec _ _); try lia. reflexivity. - -- econstructor; eauto. - * apply IHtyx3. - -- intro. rewrite bind_weaken. unfold lift_bind at 1. destruct (lt_dec _ _). - ++ eapply weakening; eauto. - ** intro. simpl. pose proof (proj2_sig i0). simpl in *. - destruct (lt_dec _ _); try tauto. f_equal. f_equal. apply le_unique. - ** econstructor; eauto. - ++ replace (ren weaken (bind σ A)) with - (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). - ** do 2 econstructor; eauto. - ** simpl. destruct (lt_dec _ _); try lia. reflexivity. - -- econstructor; eauto. - + rewrite bind_comp. replace (bind (bind σ ∘ bind_first u) B) with - (bind (bind_first (bind σ u)) (bind (lift_bind σ) B)). - * econstructor; eauto. - * rewrite bind_comp. apply bind_ext. intro. unfold lift_bind, bind_first at 2. - destruct (lt_dec _ _); simpl. - -- rewrite bind_ren. apply bind_id. intro. unfold weaken, bind_first. simpl. - pose proof (proj2_sig k). simpl in *. destruct (lt_dec _ _); try tauto. - f_equal. apply sig_lt_ext. reflexivity. - -- unfold bind_first. simpl. destruct (lt_dec _ _); try lia. reflexivity. - + econstructor; eauto. apply bind_preserves_step_equiv. assumption. + + rewrite bind_ren. rewrite bind_id; try assumption. + unfold bind_first, weaken. simpl. intro i. pose proof (proj2_sig i). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. - inversion H1; subst; clear H1. econstructor; try eassumption. apply IHtyping1. constructor. assumption. - - inversion H1; subst; clear H1. econstructor. + - inversion H1; subst; clear H1. apply srt_typing in H as typPi. + destruct typPi as [|[s typPi]]; try discriminate. + apply typ_pi_inv in typPi as [s' [s0 [sequiv [typA [typB PiCheck]]]]]. + apply srt_equiv_srt in sequiv. subst. + econstructor. + econstructor; try eassumption. apply IHtyping2. constructor. assumption. + apply bind_preserves_step_equiv_in_subs. intro. unfold bind_first. destruct (lt_dec _ _). * constructor. * apply Requiv_clot_r. constructor. assumption. - - subst. econstructor; try eassumption. apply IHtyping. constructor. assumption. + + change (Srt ?x) with (bind (bind_first (fill K t0)) (Srt x)). + eapply bind_typ; eauto using typing_imp_ctx_wf. simpl. intro. rewrite bind_ren. + rewrite bind_id. + * unfold bind_first. destruct (lt_dec _ _); try eassumption. + constructor. eapply typing_imp_ctx_wf. eassumption. + * intro. unfold bind_first, weaken. simpl. pose proof (proj2_sig k0). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + - subst. econstructor; try eassumption. apply IHtyping1. constructor. assumption. Qed. Lemma subject_reduction (Sc: pi_scheme) {n} Γ (t u : term n) A : From eebf3ab793a80f5544cd7dad1ef8b47b3b1e691f Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Sat, 29 Nov 2025 12:25:59 +0100 Subject: [PATCH 18/21] made a file to talk about weak head normal forms --- theories/LambdaCube/whnf.v | 343 +++++++++++++++++++++++++++++++++++++ 1 file changed, 343 insertions(+) create mode 100644 theories/LambdaCube/whnf.v diff --git a/theories/LambdaCube/whnf.v b/theories/LambdaCube/whnf.v new file mode 100644 index 0000000..bddea35 --- /dev/null +++ b/theories/LambdaCube/whnf.v @@ -0,0 +1,343 @@ +From Coq Require Import Utf8. +From Coq Require Import Arith Lia. +From FormArith Require Import Base. +From FormArith.LambdaCube Require Import Term Operational Typing SN. + +Reserved Notation "x w≻ y" (at level 70). +Reserved Notation "x w≻+ y" (at level 70). +Reserved Notation "x w≻* y" (at level 70). + +Inductive wctx n : Type := +| wHole : wctx n +| wApp : wctx n -> term n -> wctx n. + +Arguments wHole {n}. +Arguments wApp {n}. + +Fixpoint wfill {n} (K: wctx n) (t: term n) := + match K with + | wHole => t + | wApp K u => App (wfill K t) u + end. + +Fixpoint wctx_to_ctx {n} (K: wctx n) : ctx n n := + match K with + | wHole => Hole + | wApp K u => AppL (wctx_to_ctx K) u + end. + +Lemma fill_wctx {n} (K: wctx n) u : fill (wctx_to_ctx K) u = wfill K u. +Proof. + induction K; simpl; f_equal; auto. +Qed. + +Inductive wstep {n} : term n -> term n -> Prop := +| wctx_red {K: wctx n} {t u: term n} : t [≻] u -> wfill K t w≻ wfill K u +where "x w≻ y" := (wstep x y). + +Notation "x w≻+ y" := (Rplus wstep x y). +Notation "x w≻* y" := (Rstar wstep x y). + +Lemma wstep_is_step {n} {t u: term n} : t w≻ u -> t ≻ u. +Proof. + destruct 1. rewrite <- !fill_wctx. constructor. assumption. +Qed. + +Lemma wstep_plus_is_step_plus {n} {t u: term n} : t w≻+ u -> t ≻+ u. +Proof. + induction 1. + - econstructor; eauto using wstep_is_step. + - constructor. apply wstep_is_step. assumption. +Qed. + +Lemma wstep_star_is_step_star {n} {t u: term n} : t w≻* u -> t ≻* u. +Proof. + destruct 1. + - constructor. + - constructor. apply wstep_plus_is_step_plus. assumption. +Qed. + +Inductive neutral {n} : term n -> Prop := +| neutral_var i : neutral (Var i) +| neutral_srt s : neutral (Srt s) +| neutral_pi A B : neutral (Pi A B) +| neutral_app t u : neutral t -> neutral (App t u) +. + +Inductive whnf {n} : term n -> Prop := +| whnf_abs A t : whnf (Abs A t) +| whnf_neutral t : neutral t -> whnf t. + +Fixpoint is_neutral {n} (t: term n) : {neutral t} + {¬ neutral t} := + match t with + | Var i => left (neutral_var i) + | Pi A B => left (neutral_pi A B) + | Abs A t => right ( + fun (H: neutral (Abs A t)) => + match H in neutral t return + match t with Abs _ _ => False | _ => True end with + | neutral_var _ | _ => I + end + ) + | App t u => + match is_neutral t with + | left H => left (neutral_app t u H) + | right nneu => right ( + fun (H: neutral (App t u)) => + nneu + match H in neutral x return + match x with App t u => neutral t | _ => True end + with + | neutral_app t u H => H + | _ => I + end + ) + end + | Srt s => left (neutral_srt _) + end. + +Definition is_whnf {n} (t : term n) : {whnf t} + {¬ whnf t} := + match t with + | Abs A t => left (whnf_abs A t) + | t => + match is_neutral t with + | left H => left (whnf_neutral t H) + | right nnet => + right ( + fun (H: whnf t) => + nnet + match H in whnf t return match t with Abs _ _ => True | t => neutral t end with + | whnf_abs _ _ => I + | whnf_neutral t1 H => + match t1 as t1 + return + neutral t1 -> match t1 with Abs _ _ => True | _ => neutral t1 end + with + | Abs _ _ => fun H => I + | _ => fun H => H + end H + end + ) + end + end. + +Lemma neutral_not_wstep {n} {t u: term n} : neutral t -> ¬(t w≻ u). + induction 1 in u |- *; inversion 1; subst; destruct K; simpl in *; try discriminate; subst. + - inversion H1. + - inversion H1. + - inversion H1. + - inversion H2. subst. inversion H. + - inversion H1; subst; clear H1. eapply IHneutral. constructor. eassumption. +Qed. + +Lemma whnf_not_wstep {n} {t u: term n} : whnf t -> ¬(t w≻ u). +Proof. + destruct 1. + - inversion 1; subst. destruct K; try discriminate. simpl in *. subst. inversion H1. + - apply neutral_not_wstep. assumption. +Qed. + +Lemma not_wstep_whnf {n} {t: term n} : (forall u, ¬(t w≻ u)) -> whnf t. +Proof. + destruct t; do 2 constructor. induction t1; try constructor. + - exfalso. eapply H. change (?x w≻ ?y) with (wfill wHole x w≻ wfill wHole y). + constructor. constructor. + - eapply IHt1_1. intros ? red. inversion red. subst. eapply H. + inversion red. subst. rewrite <- H0. change (App (wfill ?K ?x) ?y) with (wfill (wApp K y) x). + constructor. eassumption. +Qed. + +Lemma SN_app : ∀ {n} {e1 e2: term n}, SN (App e1 e2) -> SN e1. +Proof. + fix IH 4. + destruct 1. constructor. intros u red. apply (IH _ _ e2). + apply (H (App u e2)). change (App ?x ?y) with (fill (AppL Hole y) x). + apply step_under_context. assumption. +Qed. + +Fixpoint wh_next_step {n} (t : term n) : option (term n) := + match t with + | App (Abs A t) u => Some (bind (bind_first u) t) + | App t u => + match wh_next_step t with + | Some t => Some (App t u) + | None => None + end + | _ => None + end. + +Lemma wh_next_step_some {n} {t u: term n} : wh_next_step t = Some u -> t w≻ u. +Proof. + induction t in u |- *; simpl; try discriminate. clear IHt2. + destruct t1; try discriminate. + - inversion 1; subst. clear H. change (?x w≻ ?y) with (wfill wHole x w≻ wfill wHole y). + constructor. constructor. + - destruct (wh_next_step _); try discriminate. intro. inversion H; subst. clear H. + specialize (IHt1 _ eq_refl). inversion IHt1. subst. + change (App (wfill K ?x) ?y) with (wfill (wApp K y) x). constructor. assumption. +Qed. + +Lemma wh_next_step_none {n} {t: term n} : wh_next_step t = None -> whnf t. +Proof. + induction t; simpl; try solve [constructor | do 2 constructor]. + destruct (wh_next_step t1). + - destruct t1; discriminate. + - specialize (IHt1 eq_refl). destruct IHt1; try discriminate. + constructor. constructor. assumption. +Qed. + +Fixpoint whnormalize_SN {n} (t: term n) (H: SN t) {struct H} : term n := + match H with + | SN_on _ H => + match wh_next_step t as x return wh_next_step t = x -> term n with + | None => fun e => t + | Some x => fun e => whnormalize_SN x (H _ (wstep_is_step (wh_next_step_some e))) + end eq_refl + end. + +Lemma whnormalize_SN_whnf {n} (t: term n) (H: SN t) : whnf (whnormalize_SN t H). +Proof. + generalize dependent n. fix IH 3. + destruct H. simpl. generalize (@eq_refl _ (wh_next_step t)). + destruct (wh_next_step t) at 2 3. + - intro. apply IH. + - apply wh_next_step_none. +Qed. + +Lemma whnormalize_SN_wstep_star {n} (t: term n) (H: SN t) : t w≻* whnormalize_SN t H. +Proof. + revert n t H. fix IH 3. destruct H; simpl. generalize (@eq_refl _ (wh_next_step t)). + destruct (wh_next_step t) at 2 3. + - intro. eapply Rstar_trans; swap 1 2. + + apply IH. + + do 2 constructor. apply wh_next_step_some. assumption. + - constructor. +Qed. + +Lemma whnormalize_SN_step_star {n} (t: term n) (H: SN t) : t ≻* whnormalize_SN t H. +Proof. + apply wstep_star_is_step_star, whnormalize_SN_wstep_star. +Qed. + +Definition whnormalize_typed {n} (t: term n) (H: exists Sc Γ T, Γ ⊢(Sc) t: T) : term n := + whnormalize_SN t ( + let '(ex_intro _ Sc (ex_intro _ Γ (ex_intro _ T H))) := H in typing_SN _ _ _ H + ). + +Lemma whnormalize_typed_whnf {n} (t: term n) (H: exists Sc Γ T, Γ ⊢(Sc) t: T) : + whnf (whnormalize_typed t H). + apply whnormalize_SN_whnf. +Qed. + +Lemma whnormalize_typed_wstep_star {n} (t: term n) (H: exists Sc Γ T, Γ ⊢(Sc) t: T) : + t w≻* whnormalize_typed t H. +Proof. + apply whnormalize_SN_wstep_star. +Qed. + +Lemma whnormalize_typed_step_star {n} (t: term n) (H: exists Sc Γ T, Γ ⊢(Sc) t: T) : + t ≻* whnormalize_typed t H. +Proof. + apply whnormalize_SN_step_star. +Qed. + +Lemma whnormalize_typed_preserves {n} (t: term n) (H: exists Sc Γ T, Γ ⊢(Sc) t: T) : + forall Sc Γ T, Γ ⊢(Sc) t : T -> Γ ⊢(Sc) whnormalize_typed t H : T. +Proof. + intros. eapply subject_reduction; try eassumption. + apply whnormalize_typed_step_star. +Qed. + +Definition whnormalize_type_of {n} (T: term n) (H: exists Sc Γ t, Γ ⊢(Sc) t: T) : term n := + match T as T return (exists _ _ _, _ ⊢(_) _: T) -> term n with + | Srt Box => fun _ => T + | T => + fun H => whnormalize_typed T ( + let '(ex_intro _ Sc (ex_intro _ Γ (ex_intro _ T H))) := H in + match srt_typing H with + | or_introl e => ltac:(discriminate) + | or_intror (ex_intro _ s H) => + ex_intro _ Sc (ex_intro _ Γ (ex_intro _ (Srt s) H)) + end + ) + end H. + +Lemma whnormalize_type_of_whnf {n} (T: term n) H : + whnf (whnormalize_type_of T H). + destruct T; simpl; try apply whnormalize_SN_whnf. destruct s; try apply whnormalize_SN_whnf. + repeat constructor. +Qed. + +Lemma whnormalize_type_of_wstep_star {n} (T: term n) (H: exists Sc Γ t, Γ ⊢(Sc) t: T) : + T w≻* whnormalize_type_of T H. +Proof. + destruct T; try apply whnormalize_SN_wstep_star. + destruct s; try apply whnormalize_SN_wstep_star. constructor. +Qed. + +Lemma whnormalize_type_of_step_star {n} (T: term n) (H: exists Sc Γ t, Γ ⊢(Sc) t: T) : + T ≻* whnormalize_type_of T H. +Proof. + apply wstep_star_is_step_star, whnormalize_type_of_wstep_star. +Qed. + +Lemma whnormalize_type_of_preserves {n} (T: term n) H : + forall Sc Γ t, Γ ⊢(Sc) t : T -> Γ ⊢(Sc) t : whnormalize_type_of T H. +Proof. + intros. apply srt_typing in H0 as H'. destruct H' as [| [s H']]. + - subst. simpl. assumption. + - econstructor; try eassumption. + + apply Requiv_clot_star, whnormalize_type_of_step_star. + + eapply subject_reduction; try eassumption. apply whnormalize_type_of_step_star. +Qed. + +Lemma neutral_not_redex {n} (t u: term n) : neutral t -> ¬ (t [≻] u). + intro H. inversion 1; subst. inversion_clear H. inversion H1. +Qed. + +Lemma neutral_step {n} (t u : term n) : neutral t -> t ≻ u -> neutral u. +Proof. + induction 1 in u |- *; inversion 1; subst; destruct K; try discriminate; simpl in *; + try solve [constructor]; subst; try solve [match goal with H: _ [≻] _ |- _ => inversion H end]. + - exfalso. eapply neutral_not_redex; [| eassumption]. constructor. assumption. + - inversion H1; subst; clear H1. constructor. apply IHneutral. constructor. assumption. + - inversion H1; subst; clear H1. constructor. assumption. +Qed. + +Lemma neutral_step_plus {n} (t u : term n) : neutral t -> t ≻+ u -> neutral u. +Proof. + induction 2; eapply neutral_step; eauto. +Qed. + +Lemma neutral_step_star {n} (t u : term n) : neutral t -> t ≻* u -> neutral u. +Proof. + destruct 2; eauto using neutral_step_plus. +Qed. + +Lemma neutral_app_step {n} (t1 t2 u: term n) : + neutral t1 -> App t1 t2 ≻ u -> exists u1 u2, u = App u1 u2. +Proof. + inversion 2; subst. destruct K; simpl in *; try discriminate; eauto. subst. exfalso. + eapply neutral_not_redex; [| eassumption]. constructor. assumption. +Qed. + +Lemma neutral_app_step_star {n} (t1 t2 u: term n) : + neutral t1 -> App t1 t2 ≻* u -> exists u1 u2, u = App u1 u2. +Proof. + destruct 2; eauto. induction H0. + - apply neutral_step_plus in H0; [| constructor; assumption]. clear H. firstorder subst. + inversion_clear H0. eapply neutral_app_step; try eassumption. + - eapply neutral_app_step; try eassumption. +Qed. + +Lemma whnf_is_pi_type_or_never_will_be {n} {t: term n} : + whnf t -> + match t with Pi _ _ => True | _ => forall A B, ¬ (t ≅ Pi A B) end. +Proof. + destruct t; auto; intros H ? ? e; apply Requiv_sym, pi_equiv in e as [A' [B' [eA [eB e]]]]. + - apply var_star in e. discriminate. + - apply abs_star in e. firstorder discriminate. + - inversion_clear H. inversion_clear H0. apply neutral_app_step_star in e; auto. + firstorder discriminate. + - apply srt_star in e. discriminate. +Qed. From 79c358aef26f8db013717f1fa9c5327ead32033d Mon Sep 17 00:00:00 2001 From: Bousmaha Wassel Date: Fri, 5 Dec 2025 23:00:57 +0100 Subject: [PATCH 19/21] wrote type inference for the lambda cube --- theories/LambdaCube/Typing.v | 65 +++-- theories/LambdaCube/infer.v | 419 ++++++++++++++++++++++++++++++++ theories/LambdaCube/normalize.v | 210 ++++++++++++++++ theories/LambdaCube/whnf.v | 12 + 4 files changed, 671 insertions(+), 35 deletions(-) create mode 100644 theories/LambdaCube/infer.v create mode 100644 theories/LambdaCube/normalize.v diff --git a/theories/LambdaCube/Typing.v b/theories/LambdaCube/Typing.v index 44b3e5d..4caf32d 100644 --- a/theories/LambdaCube/Typing.v +++ b/theories/LambdaCube/Typing.v @@ -8,9 +8,7 @@ Inductive typing_ctx : nat -> Type := | cons {n} : typing_ctx n -> term n -> typing_ctx (S n). Notation "\" := empty. -Notation "A , t" := (cons A t) (at level 61, left associativity, t at next level). - -Search (_ < S _ -> {_} + {_}). +Notation "A ; t" := (cons A t) (at level 61, left associativity, t at next level). Fixpoint kth_index_ctx {n} (Γ: typing_ctx n) k {struct Γ} : k < n -> term n := match Γ in typing_ctx n return k < n -> term n with @@ -37,12 +35,12 @@ Inductive typing (P: pi_scheme) : forall {n}, typing_ctx n -> term n -> term n - | typ_var {n} {Γ: typing_ctx n} {i} : Γ ⊢(P) -> Γ ⊢(P) Var i : kth_index_ctx Γ (proj1_sig i) (proj2_sig i) | typ_pi {n} {Γ: typing_ctx n} {A B s s'} : - pi_scheme_check P s s' -> Γ ⊢(P) A : Srt s -> Γ, A ⊢(P) B : Srt s' -> Γ ⊢(P) Pi A B : Srt s' + pi_scheme_check P s s' -> Γ ⊢(P) A : Srt s -> Γ; A ⊢(P) B : Srt s' -> Γ ⊢(P) Pi A B : Srt s' | typ_abs {n} {Γ: typing_ctx n} {A B s s' t} : pi_scheme_check P s s' -> Γ ⊢(P) A : Srt s -> - Γ, A ⊢(P) B : Srt s' -> - Γ, A ⊢(P) t : B -> + Γ; A ⊢(P) B : Srt s' -> + Γ; A ⊢(P) t : B -> Γ ⊢(P) Abs A t : Pi A B | typ_app {n} {Γ: typing_ctx n} {A B t u} : Γ ⊢(P) t : Pi A B -> Γ ⊢(P) u : A -> Γ ⊢(P) App t u : bind (bind_first u) B @@ -51,7 +49,7 @@ Inductive typing (P: pi_scheme) : forall {n}, typing_ctx n -> term n -> term n - with ctx_wf (P: pi_scheme) : forall {n}, typing_ctx n -> Prop := | empty_wf : \ ⊢(P) | cons_wf {n} {A: typing_ctx n} {t: term n} {s} : - A ⊢(P) -> A ⊢(P) t : Srt s -> A, t ⊢(P) + A ⊢(P) -> A ⊢(P) t : Srt s -> A; t ⊢(P) where "A ⊢( P ) t ':' s" := (typing P A t s) and "A ⊢( P )" := (ctx_wf P A) . @@ -117,7 +115,7 @@ Qed. Lemma typ_pi_inv Sc {n} (Γ : typing_ctx n) A B T : Γ ⊢(Sc) Pi A B : T -> exists s s', - T ≅ Srt s' /\ Γ ⊢(Sc) A : Srt s /\ Γ, A ⊢(Sc) B : Srt s' /\ pi_scheme_check Sc s s'. + T ≅ Srt s' /\ Γ ⊢(Sc) A : Srt s /\ Γ; A ⊢(Sc) B : Srt s' /\ pi_scheme_check Sc s s'. Proof. remember (Pi A B). induction 1 in A, B, Heqt |- *; try discriminate. - exists s. exists s'. inversion Heqt; subst; clear Heqt. intuition constructor. @@ -128,7 +126,7 @@ Qed. Lemma typ_abs_inv Sc {n} (Γ: typing_ctx n) A t T : Γ ⊢(Sc) Abs A t : T -> exists s s' B X, - T ≅ Pi A B /\ Γ ⊢(Sc) A : Srt s /\ Γ, A ⊢(Sc) B : Srt s' /\ Γ, A ⊢(Sc) t : B /\ + T ≅ Pi A B /\ Γ ⊢(Sc) A : Srt s /\ Γ; A ⊢(Sc) B : Srt s' /\ Γ; A ⊢(Sc) t : B /\ Γ ⊢(Sc) T : X /\ pi_scheme_check Sc s s'. Proof. remember (Abs A t). @@ -216,7 +214,7 @@ Lemma gen_weakening {Sc n k} {σ: {i | i < n} -> {i | i < k}} {Γ Γ' x T} : Qed. Lemma weakening {Sc n} {Γ: typing_ctx n} {A x T s}: - Γ ⊢(Sc) x : T -> Γ ⊢(Sc) A : Srt s -> Γ, A ⊢(Sc) ren weaken x : ren weaken T. + Γ ⊢(Sc) x : T -> Γ ⊢(Sc) A : Srt s -> Γ; A ⊢(Sc) ren weaken x : ren weaken T. Proof. intros. eapply gen_weakening; eauto. - destruct i; simpl. destruct (lt_dec _ _); try tauto. f_equal. f_equal. apply le_unique. @@ -289,7 +287,7 @@ Lemma bind_typ Sc n k (σ : {i | i < k} -> term n) Γ Γ' x T : * rewrite bind_weaken. eapply weakening; eauto. * rewrite bind_weaken. replace (ren weaken (bind σ A)) with - (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). + (kth_index_ctx (Γ; bind σ A) n (Nat.lt_succ_diag_r n)). -- constructor. econstructor; eauto. -- simpl. destruct (lt_dec n n); try lia. reflexivity. + econstructor; eauto. @@ -299,7 +297,7 @@ Lemma bind_typ Sc n k (σ : {i | i < k} -> term n) Γ Γ' x T : destruct (lt_dec _ _). -- eapply weakening; eauto. -- replace (ren weaken (bind σ A)) with - (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). + (kth_index_ctx (Γ; bind σ A) n (Nat.lt_succ_diag_r n)). ++ do 2 econstructor; eauto. ++ simpl. destruct (lt_dec _ _); try lia. reflexivity. * econstructor; eauto. @@ -307,7 +305,7 @@ Lemma bind_typ Sc n k (σ : {i | i < k} -> term n) Γ Γ' x T : * intro. rewrite bind_weaken. unfold lift_bind at 1. destruct (lt_dec _ _). -- eapply weakening; eauto. -- replace (ren weaken (bind σ A)) with - (kth_index_ctx (Γ, bind σ A) n (Nat.lt_succ_diag_r n)). + (kth_index_ctx (Γ; bind σ A) n (Nat.lt_succ_diag_r n)). ++ do 2 econstructor; eauto. ++ simpl. destruct (lt_dec _ _); try lia. reflexivity. * econstructor; eauto. @@ -323,6 +321,21 @@ Lemma bind_typ Sc n k (σ : {i | i < k} -> term n) Γ Γ' x T : - econstructor; eauto. apply bind_preserves_step_equiv. assumption. Qed. +Lemma bind_first_typ {Sc n Γ} {u: term n} {t U T} : + Γ ⊢(Sc) u : U -> Γ; U ⊢(Sc) t : T -> Γ ⊢(Sc) bind (bind_first u) t : bind (bind_first u) T. +Proof. + intros. assert (Γ ⊢(Sc)) by (eapply typing_imp_ctx_wf; eassumption). + eapply bind_typ; try eassumption. + intro. simpl. unfold bind_first at 1. destruct (lt_dec _ _). + - rewrite bind_ren. rewrite bind_id. + + constructor. assumption. + + intro. unfold weaken, bind_first. simpl. pose proof (proj2_sig k). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + - rewrite bind_ren. rewrite bind_id; try assumption. + intro. unfold weaken, bind_first. simpl. pose proof (proj2_sig k). simpl in *. + destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. +Qed. + Lemma typed_imp_subterm_typed {Sc} {n k} {Γ u T} {K: ctx k n} : Γ ⊢(Sc) fill K u : T -> exists Γ' T', Γ' ⊢(Sc) u : T'. remember (fill K u) as t. induction 1 in k, u, K, Heqt |- *. @@ -382,12 +395,7 @@ Proof. apply typ_pi_inv in IHtyping1 as [s' [s'' [equiv_srts [typA [typB Sc_check]]]]]. apply srt_equiv_srt in equiv_srts. subst. rename s' into s, s'' into s'. change (Srt s') with (bind (bind_first u) (Srt s')). - eapply bind_typ; try eassumption. - * intro. unfold bind_first at 1. simpl. rewrite bind_ren. rewrite bind_id. - { destruct (lt_dec _ _); try assumption. constructor. eauto using typing_imp_ctx_wf. } - clear. destruct k. unfold bind_first. simpl. destruct (lt_dec x n); try tauto. - f_equal. apply sig_lt_ext. reflexivity. - * eauto using typing_imp_ctx_wf. + eapply bind_first_typ; try eassumption. - destruct IHtyping1. + subst. apply srt_equiv in H0. left. clear IHtyping2. clear dependent t. apply @no_spontaneous_srt_step_star with (K := Hole) in H0 as [k [K e]]. subst. @@ -463,7 +471,7 @@ Proof. destruct H as [Hequiv [type_ty [type_B0 [type_body [typ_piAB pi_check]]]]]. apply pi_equiv_pi in Hequiv as [Aequiv Bequiv]. apply typ_pi_inv in typ_piAB as [s0 [s0' [Xequiv [typA [typB pi_check2]]]]]. - assert (true_type_body : Γ, ty ⊢(Sc) body : B). + assert (true_type_body : Γ; ty ⊢(Sc) body : B). { econstructor; eauto using Requiv_sym. eapply equiv_context; try eassumption. - simpl. intros. apply ren_preserves_step_equiv. destruct (lt_dec _ _); auto using Requiv_sym. constructor. @@ -479,15 +487,7 @@ Proof. assert (true_type_u : Γ ⊢(Sc) u : ty). { econstructor; eauto. } revert true_type_body true_type_u. clear. intros tybody tyu. - eapply bind_typ; eauto using typing_imp_ctx_wf. - intro. destruct i; simpl. unfold bind_first at 1. simpl. destruct (lt_dec _ _). - + rewrite bind_ren. rewrite bind_id. - * constructor. eapply typing_imp_ctx_wf; eassumption. - * unfold bind_first, weaken. simpl. intro i. pose proof (proj2_sig i). simpl in *. - destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. - + rewrite bind_ren. rewrite bind_id; try assumption. - unfold bind_first, weaken. simpl. intro i. pose proof (proj2_sig i). simpl in *. - destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + eapply bind_first_typ; eassumption. - inversion H1; subst; clear H1. econstructor; try eassumption. apply IHtyping1. constructor. assumption. - inversion H1; subst; clear H1. apply srt_typing in H as typPi. @@ -501,12 +501,7 @@ Proof. * constructor. * apply Requiv_clot_r. constructor. assumption. + change (Srt ?x) with (bind (bind_first (fill K t0)) (Srt x)). - eapply bind_typ; eauto using typing_imp_ctx_wf. simpl. intro. rewrite bind_ren. - rewrite bind_id. - * unfold bind_first. destruct (lt_dec _ _); try eassumption. - constructor. eapply typing_imp_ctx_wf. eassumption. - * intro. unfold bind_first, weaken. simpl. pose proof (proj2_sig k0). simpl in *. - destruct (lt_dec _ _); try tauto. f_equal. apply sig_lt_ext. reflexivity. + eapply bind_first_typ; eassumption. - subst. econstructor; try eassumption. apply IHtyping1. constructor. assumption. Qed. diff --git a/theories/LambdaCube/infer.v b/theories/LambdaCube/infer.v new file mode 100644 index 0000000..56d15f5 --- /dev/null +++ b/theories/LambdaCube/infer.v @@ -0,0 +1,419 @@ +From Coq Require Import Utf8. +From Coq Require Import Arith Lia. +From FormArith Require Import Base. +From FormArith.LambdaCube Require Import Term Operational Typing SN whnf normalize. + +Inductive strong_ctx_wf (Sc: pi_scheme) : forall {n}, typing_ctx n -> Type := +| strong_empty_wf : strong_ctx_wf Sc \ +| strong_cons_wf {n} {Γ: typing_ctx n} {A: term n} s : + strong_ctx_wf Sc Γ -> Γ ⊢(Sc) A : Srt s -> strong_ctx_wf Sc (Γ; A) +. + +Lemma strong_to_weak_ctx_wf Sc {n} (Γ: typing_ctx n) : strong_ctx_wf Sc Γ -> Γ ⊢(Sc). +Proof. + induction 1; econstructor; eassumption. +Qed. + +Fixpoint kth_srt_ctx {Sc} {n} {Γ: typing_ctx n} (H: strong_ctx_wf Sc Γ) (k: nat) {struct H} + : k < n -> sort := + match H with + | strong_empty_wf _ => fun H => match Nat.nlt_0_r k H with end + | @strong_cons_wf _ n _ _ s H _ => + fun _ => + match lt_dec k n with + | left l => kth_srt_ctx H k l + | right _ => s + end + end. + +Lemma kth_typ_index {Sc} {n} {Γ: typing_ctx n} (H: strong_ctx_wf Sc Γ) k (l : k < n) : + Γ ⊢(Sc) kth_index_ctx Γ k l : Srt (kth_srt_ctx H k l). +Proof. + induction H; simpl. { destruct (Nat.nlt_0_r _ _). } destruct (lt_dec _ _). + - change (@Srt (S ?n) ?s) with (ren weaken (@Srt n s)). eapply weakening; eauto. + - change (@Srt (S ?n) ?s) with (ren weaken (@Srt n s)). eapply weakening; eassumption. +Qed. + +Lemma SN_srt {n} s : SN (@Srt n s). +Proof. + constructor. intros. exfalso. eapply no_srt_step. eassumption. +Qed. + +Inductive infer_ret Sc {n} Γ (t: term n) : Type := +| Untyped +| Kind (typt: Γ ⊢(Sc) t : Srt Box) +| Sorted T s (typt: Γ ⊢(Sc) t : T) (typT: Γ ⊢(Sc) T : Srt s). + +Arguments Kind {_ _ _ _}. +Arguments Sorted {_ _ _ _}. + +(* Sorted means we have a term that is neither a type nor a kind, along with its sort *) + +Fixpoint infer_aux Sc {n} {Γ} (H: strong_ctx_wf Sc Γ) (t: term n) {struct t} + : infer_ret Sc Γ t := + match t with + | Srt Star => Kind (typ_star _ (strong_to_weak_ctx_wf _ _ H)) + | Srt Box => Untyped _ _ _ + | Var k => + (*match kth_index_ctx Γ (proj1_sig k) (proj2_sig k) + as T return + Γ ⊢(Sc) Var k : T -> + Γ ⊢(Sc) T : Srt (kth_srt_ctx H (proj1_sig k) (proj2_sig k)) -> _ + with + | Srt Star => fun H _ => _ + | T => fun typV typT => Sorted T _ typV typT + end*) Sorted _ _ (typ_var _ (strong_to_weak_ctx_wf _ _ H)) (kth_typ_index H _ _) + | Pi A B => + match infer_aux Sc H A with + | Kind typA => + match infer_aux Sc (strong_cons_wf _ _ H typA) B with + | Kind typB => + (if Sc Box Box as b return Sc Box Box = b -> _ + then fun e => Kind (typ_pi _ e typA typB) + else fun _ => Untyped _ _ _) eq_refl + | Sorted T s' typB typT => + let H' := ex_intro _ _ (ex_intro _ _ (ex_intro _ _ typT)) in + match whnormalize_typed T H' as T' return Γ; A ⊢(Sc) B : T' -> _ + with + | Srt Star => + fun typB => + (if Sc Box Star as b return Sc Box Star = b -> _ + then fun e => + Sorted _ _ (typ_pi _ e typA typB) + (typ_star _ (strong_to_weak_ctx_wf _ _ H)) + else fun _ => Untyped _ _ _) eq_refl + | _ => fun _ => Untyped _ _ _ + end ( + let H' : T ≻* whnormalize_typed T H' := whnormalize_typed_step_star _ _ in + typ_conv _ typB (Requiv_clot_star H') (subject_reduction _ _ _ _ _ typT H') + ) + | _ => Untyped _ _ _ + end + | Sorted T s typA typT => + let H' := ex_intro _ _ (ex_intro _ _ (ex_intro _ _ typT)) in + match whnormalize_typed T H' as T' return Γ ⊢(Sc) A : T' -> _ + with + | Srt Star => + fun typA => + match infer_aux Sc (strong_cons_wf _ _ H typA) B with + | Kind typB => + (if Sc Star Box as b return Sc Star Box = b -> _ + then fun e => Kind (typ_pi _ e typA typB) + else fun _ => Untyped _ _ _) eq_refl + | Sorted T s' typB typT => + let H' := ex_intro _ _ (ex_intro _ _ (ex_intro _ _ typT)) in + match whnormalize_typed T H' as T' return Γ; A ⊢(Sc) B : T' -> _ + with + | Srt Star => + fun typB => + (if Sc Star Star as b return Sc Star Star = b -> _ + then fun e => + Sorted _ _ (typ_pi _ e typA typB) + (typ_star _ (strong_to_weak_ctx_wf _ _ H)) + else fun _ => Untyped _ _ _) eq_refl + | _ => fun _ => Untyped _ _ _ + end ( + let H' : T ≻* whnormalize_typed T H' := whnormalize_typed_step_star _ _ + in typ_conv _ typB (Requiv_clot_star H') + (subject_reduction _ _ _ _ _ typT H') + ) + | _ => Untyped _ _ _ + end + | _ => fun _ => Untyped _ _ _ + end ( + let H' : T ≻* whnormalize_typed T H' := whnormalize_typed_step_star _ _ in + typ_conv _ typA (Requiv_clot_star H') (subject_reduction _ _ _ _ _ typT H') + ) + | _ => Untyped _ _ _ + end + | Abs A t => + match infer_aux Sc H A with + | Kind typA => + match infer_aux Sc (strong_cons_wf _ _ H typA) t with + | Kind typt => Untyped _ _ _ + | Sorted B s' typt typB => + (if Sc Box s' as b return Sc Box s' = b -> _ + then fun e => + Sorted _ _ + (typ_abs _ e typA typB typt) + (typ_pi _ e typA typB) + else fun _ => Untyped _ _ _) eq_refl + | _ => Untyped _ _ _ + end + | Sorted T s typA typT => + let H' := ex_intro _ _ (ex_intro _ _ (ex_intro _ _ typT)) in + match whnormalize_typed T H' as T' return Γ ⊢(Sc) A : T' -> _ + with + | Srt Star => + fun typA => + match infer_aux Sc (strong_cons_wf _ _ H typA) t with + | Kind typt => Untyped _ _ _ + | Sorted B s' typt typB => + (if Sc Star s' as b return Sc Star s' = b -> _ + then fun e => + Sorted _ _ + (typ_abs _ e typA typB typt) + (typ_pi _ e typA typB) + else fun _ => Untyped _ _ _) eq_refl + | _ => Untyped _ _ _ + end + | _ => fun _ => Untyped _ _ _ + end ( + let H' : T ≻* whnormalize_typed T H' := whnormalize_typed_step_star _ _ in + typ_conv _ typA (Requiv_clot_star H') (subject_reduction _ _ _ _ _ typT H') + ) + | _ => Untyped _ _ _ + end + | App t u => + match infer_aux Sc H t with + | Sorted T s' typt typT => + let H' := ex_intro _ _ (ex_intro _ _ (ex_intro _ _ typT)) in + match whnormalize_typed T H' as T' return Γ ⊢(Sc) t : T' -> Γ ⊢(Sc) T' : Srt s' -> _ + with + | Pi A B => + fun typt typPi => + (fun H' : exists s, Γ ⊢(Sc) A : Srt s /\ Γ ; A ⊢(Sc) B: Srt s' => + match infer_aux Sc H u with + | Sorted U s typu typU => + match convertible_typed (ex_intro _ _ typU) + (let (s, H') := H' in + let (typA, _) := H' in + ex_intro _ _ typA) + with + | left Hconv => + Sorted _ _ + (typ_app _ typt + (let (_, H') := H' in + let (typA, _) := H' in + typ_conv _ typu Hconv typA + )) + (let (_, H') := H' in + let (typA, typB) := H' in + bind_first_typ (typ_conv _ typu Hconv typA) typB : + (Γ ⊢(Sc) _ : bind (bind_first u) (Srt s')) + ) + | right _ => Untyped _ _ _ + end + (* -2 Goal *) + | Kind typu => + Untyped _ _ _ + | _ => Untyped _ _ _ + end + ) + ( + let (s, H') := typ_pi_inv _ _ _ _ _ typPi in + let (s__c, H') := H' in + let (srt_eq, H') := H' in + let (typA, H') := H' in + let (typB, _) := H' in + ex_intro _ s ( + conj typA + ( + let e := srt_equiv_srt srt_eq in + match eq_sym e with + | eq_refl => typB + end + ) + ) + ) + | _ => fun _ _ => Untyped _ _ _ + end + (typ_conv _ typt (Requiv_clot_star (whnormalize_typed_step_star _ _)) + (whnormalize_typed_preserves _ _ _ _ _ typT) + ) + (whnormalize_typed_preserves _ _ _ _ _ typT) + | _ => Untyped _ _ _ + end + end. + +Lemma typed_infer_aux_not_untyped Sc {n} Γ (H: strong_ctx_wf Sc Γ) (t T: term n) : + Γ ⊢(Sc) t : T -> match infer_aux Sc H t with Untyped _ _ _ => False | _ => True end. +Proof. + induction 1; simpl; auto. + - specialize (IHtyping1 H). destruct (infer_aux _ _ A) as [| typA |]; try tauto. + + assert (s = Box). + { eapply srt_equiv_srt. eapply unique_typing; eassumption. } subst. + clear H0_. rename H0 into pi_check. + specialize (IHtyping2 (strong_cons_wf _ _ H typA)). + destruct (infer_aux _ _ _); try tauto. + * generalize (@eq_refl _ (Sc Box Box)). generalize (Sc Box Box) at 2 3. + destruct b; try tauto. intro. unfold pi_scheme_check in *. + assert (s' = Box). + { eapply srt_equiv_srt. eapply unique_typing; eassumption. } + subst. congruence. + * assert (T ≻* Srt s'). + { eapply srt_equiv. eapply unique_typing; try eassumption. } + match goal with |- context[match _ with _ => _ end ?x] => generalize x end. + set (whnormalize_typed _ _). + assert (t ≻* Srt s'). + { eapply confluence_step in H0 as [v [norm_red srt_red]]; swap 1 2. + { apply whnormalize_typed_step_star. } apply srt_star in srt_red. subst. + exact norm_red. } + assert (t ≅ Srt s'). + { apply Requiv_clot_star. assumption. } + assert (t = Srt s'). + { pose proof (whnft := whnormalize_typed_whnf _ _ : whnf t). + epose proof (whnf_is_sort_type_or_never_will_be whnft). + destruct t; try firstorder. f_equal. eapply srt_equiv_srt. eassumption. } + rewrite H3. + assert (typs' : Γ; A ⊢(Sc) Srt s' : Srt s). + { eapply subject_reduction; try eassumption. } + assert (s' = Star). + { destruct s'; auto. exfalso. revert typs'. clear. generalize (@Srt (S n) s) as T. intro. + remember (Srt Box). induction 1 in Heqt |- *; try discriminate; tauto. } + subst. intro. generalize (@eq_refl _ (Sc Box Star)). + generalize (Sc Box Star) at 2 3. destruct b; auto. congruence. + + assert (T ≻* Srt s). + { eapply srt_equiv. eapply unique_typing; try eassumption. } + match goal with |- context[match _ with _ => _ end ?x] => generalize x end. + set (whnormalize_typed _ _). + assert (t ≻* Srt s). + { eapply confluence_step in H1 as [v [norm_red srt_red]]; swap 1 2. + { apply whnormalize_typed_step_star. } apply srt_star in srt_red. subst. + exact norm_red. } + assert (t ≅ Srt s). + { apply Requiv_clot_star. assumption. } + assert (t = Srt s). + { pose proof (whnft := whnormalize_typed_whnf _ _ : whnf t). + epose proof (whnf_is_sort_type_or_never_will_be whnft). + destruct t; try firstorder. f_equal. eapply srt_equiv_srt. eassumption. } + rewrite H4. clear dependent t. + assert (typs : Γ ⊢(Sc) Srt s : Srt s0) by (eauto using subject_reduction). + assert (s = Star). + { destruct s; auto. exfalso. revert typs. clear. generalize (@Srt (S n) s0) as T. intro. + remember (Srt Box). clear T. induction 1 in Heqt |- *; try discriminate; tauto. } + subst. intro typA. clear dependent T. + specialize (IHtyping2 (strong_cons_wf _ _ H typA)). destruct (infer_aux _ _ _); try tauto. + * generalize (@eq_refl _ (Sc Star Box)). generalize (Sc Star Box) at 2 3. + destruct b; try tauto. intro. unfold pi_scheme_check in *. + assert (s' = Box). + { eapply srt_equiv_srt. eapply unique_typing; eassumption. } + subst. congruence. + * assert (T ≻* Srt s'). + { eapply srt_equiv. eapply unique_typing; try eassumption. } + match goal with |- context[match _ with _ => _ end ?x] => generalize x end. + set (whnormalize_typed _ _). + assert (t ≻* Srt s'). + { eapply confluence_step in H1 as [v [norm_red srt_red]]; swap 1 2. + { apply whnormalize_typed_step_star. } apply srt_star in srt_red. subst. + exact norm_red. } + assert (t ≅ Srt s'). + { apply Requiv_clot_star. assumption. } + assert (t = Srt s'). + { pose proof (whnft := whnormalize_typed_whnf _ _ : whnf t). + epose proof (whnf_is_sort_type_or_never_will_be whnft). + destruct t; try firstorder. f_equal. eapply srt_equiv_srt. eassumption. } + rewrite H4. + assert (typs' : Γ; A ⊢(Sc) Srt s' : Srt s). + { eapply subject_reduction; try eassumption. } + assert (s' = Star). + { destruct s'; auto. exfalso. revert typs'. clear. generalize (@Srt (S n) s) as T. intro. + remember (Srt Box). induction 1 in Heqt |- *; try discriminate; tauto. } + subst. intro. generalize (@eq_refl _ (Sc Star Star)). + generalize (Sc Star Star) at 2 3. destruct b; auto. congruence. + - specialize (IHtyping1 H). destruct (infer_aux _ _ A); try tauto. + + specialize (IHtyping3 (strong_cons_wf _ Box H typt)). + destruct (infer_aux _ _ _); try tauto. + * cut (Γ; A ⊢(Sc) Srt Box : Srt s'). + { clear. remember (Srt Box). induction 1 in Heqt |- *; try discriminate; tauto. } + eapply subject_reduction; try eassumption. eapply srt_equiv. + eapply unique_typing; try eassumption. + * generalize (@eq_refl _ (Sc Box s0)). generalize (Sc Box s0) at 2 3. + destruct b; auto. + assert (s = Box). {eapply srt_equiv_srt. eapply unique_typing; eassumption. } + subst. enough (s' = s0) by congruence. + assert (T ≅ B) by eauto using unique_typing. + apply (@srt_equiv_srt (S n)). revert H0_0 typT H1. + generalize (Γ; A) (@Srt (S n) s') (@Srt (S n) s0). clear. + rename B into t, T into u. intros Γ X Y typB typT Hcong. + eapply equiv_both_star in Hcong as [v [redu redt]]. + eapply unique_typing; eapply subject_reduction; eauto. + + assert (T ≻* Srt s). + { eapply srt_equiv. eapply unique_typing; try eassumption. } + match goal with |- context[match _ with _ => _ end ?x] => generalize x end. + set (whnormalize_typed _ _) as u. + assert (u ≻* Srt s). + { eapply confluence_step in H1 as [v [norm_red srt_red]]; swap 1 2. + { apply whnormalize_typed_step_star. } apply srt_star in srt_red. subst. + exact norm_red. } + assert (u ≅ Srt s). + { apply Requiv_clot_star. assumption. } + assert (u = Srt s). + { pose proof (whnfu := whnormalize_typed_whnf _ _ : whnf u). + epose proof (whnf_is_sort_type_or_never_will_be whnfu). + destruct u; try firstorder. f_equal. eapply srt_equiv_srt. eassumption. } + rewrite H4. clear dependent u. + assert (typs : Γ ⊢(Sc) Srt s : Srt s0) by (eauto using subject_reduction). + assert (s = Star). + { destruct s; auto. exfalso. revert typs. clear. generalize (@Srt (S n) s0) as T. intro. + remember (Srt Box). clear T. induction 1 in Heqt |- *; try discriminate; tauto. } + subst. intro typA. clear dependent T. + specialize (IHtyping3 (strong_cons_wf _ _ H typA)). destruct (infer_aux _ _ _); try tauto. + * cut (Γ; A ⊢(Sc) Srt Box : Srt s'). + { clear. remember (Srt Box). induction 1 in Heqt |- *; try discriminate; tauto. } + eapply subject_reduction; try eassumption. eapply srt_equiv. + eapply unique_typing; try eassumption. + * generalize (@eq_refl _ (Sc Star s)). generalize (Sc Star s) at 2 3. + destruct b; auto. + enough (s = s') by congruence. + assert (T ≅ B) by eauto using unique_typing. + apply (@srt_equiv_srt (S n)). revert H0_0 typT H1. + generalize (Γ; A) (@Srt (S n) s') (@Srt (S n) s0). clear. + rename B into t, T into u. intros Γ X Y typB typT Hcong. + eapply equiv_both_star in Hcong as [v [redu redt]]. + eapply unique_typing; eapply subject_reduction; eauto. + - specialize (IHtyping1 H). destruct (infer_aux _ _ t); try tauto. + { assert (e: Srt Box ≅ Pi A B) by eauto using unique_typing. + eapply srt_equiv, pi_star in e. firstorder discriminate. } + match goal with |- context[match _ with _ => _ end ?x ?y] => generalize x y end. + set (whnormalize_typed _ _) as T'. + pose proof (whnft := whnormalize_typed_whnf _ _ : whnf T'). + epose proof (whnf_is_pi_type_or_never_will_be whnft). intros typt' typT'. + assert (T' ≅ Pi A B) by eauto using unique_typing. + match goal with |- context[match _ with _ => _ end ?x typT'] => generalize x end. + destruct T'; try solve [firstorder]. intro typt''. + specialize (IHtyping2 H). destruct (infer_aux _ _ _); try tauto. + { assert (Hcong : A ≅ Srt Box) by eauto using unique_typing. revert H0_ Hcong. clear. + intros Htyp Hcong. apply srt_typing in Htyp as [|[s Htyp]]; try discriminate. + apply typ_pi_inv in Htyp as [s' [_ [_ [typA _]]]]. apply Requiv_sym, srt_equiv in Hcong. + assert (c : Γ ⊢(Sc) Srt Box: Srt s') by eauto using subject_reduction. + revert c. clear. remember (Srt Box). induction 1; try discriminate; tauto. } + destruct (convertible_typed _ _); auto. + apply n0. assert (Hcong : T0 ≅ A) by eauto using unique_typing. + apply (Requiv_trans Hcong). revert H1. clear. intro H. apply pi_equiv_pi in H. + intuition auto using Requiv_sym. + - apply IHtyping1. +Qed. + +Definition infer Sc {n} {Γ} (H: strong_ctx_wf Sc Γ) (t: term n) : option (term n) := + match infer_aux Sc H t with + | Untyped _ _ _ => None + | Kind _ => Some (Srt Box) + | Sorted T _ _ _ => Some T + end. + +Lemma infer_some Sc {n} {Γ} (H: strong_ctx_wf Sc Γ) (t: term n) T : + infer Sc H t = Some T -> Γ ⊢(Sc) t : T. +Proof. + unfold infer. + destruct (infer_aux _ _ _); try discriminate; inversion 1; subst; auto. +Qed. + +Lemma infer_none Sc {n} {Γ} (H: strong_ctx_wf Sc Γ) (t: term n) : + infer Sc H t = None -> forall T, ¬ (Γ ⊢(Sc) t : T). +Proof. + unfold infer. + destruct (infer_aux _ _) eqn: e; try discriminate. intros _ T typt. + eapply typed_infer_aux_not_untyped in typt. rewrite e in typt. assumption. +Qed. + +Definition infer_dec Sc {n} {Γ} (H: strong_ctx_wf Sc Γ) (t: term n) : + { T | Γ ⊢(Sc) t : T } + {forall T, ¬ (Γ ⊢(Sc) t : T)} := + match infer Sc H t as o return infer Sc H t = o -> _ with + | None => fun e => inright (infer_none _ _ _ e) + | Some T => fun e => inleft (exist _ T (infer_some _ _ _ _ e)) + end eq_refl. + +Definition infer_dec_closed Sc (t: term 0) : + { T | \ ⊢(Sc) t : T } + {forall T, ¬ (\ ⊢(Sc) t : T)} := + infer_dec Sc (strong_empty_wf Sc) t. diff --git a/theories/LambdaCube/normalize.v b/theories/LambdaCube/normalize.v new file mode 100644 index 0000000..0393d62 --- /dev/null +++ b/theories/LambdaCube/normalize.v @@ -0,0 +1,210 @@ +From Coq Require Import Utf8. +From Coq Require Import Arith Lia. +From FormArith Require Import Base. +From FormArith.LambdaCube Require Import Term Operational Typing SN whnf. + +Fixpoint next_step {n} (t: term n) : option (term n) := + match t with + | Var _ | Srt _ => None + | Pi A B => + match next_step A with + | Some A' => Some (Pi A' B) + | None => match next_step B with + | Some B' => Some (Pi A B') + | None => None + end + end + | Abs A t => + match next_step A with + | Some A' => Some (Abs A' t) + | None => match next_step t with + | Some t' => Some (Abs A t') + | None => None + end + end + | App t u => + match next_step t with + | Some t' => Some (App t' u) + | None => match next_step u with + | Some u' => Some (App t u') + | None => match t with + | Abs _ f => Some (bind (bind_first u) f) + | _ => None + end + end + end + end. + +Lemma next_step_some {n} {t t' : term n} : next_step t = Some t' -> t ≻ t'. +Proof. + induction t; simpl; try discriminate. + all: destruct (next_step t1); + [ + specialize (IHt1 _ eq_refl) | + destruct (next_step t2); try discriminate; try specialize (IHt2 _ eq_refl) + ]; intro e; inversion e; subst; clear e. + - apply step_under_context with (K := PiL Hole t2). assumption. + - apply step_under_context with (K := PiR t1 Hole). assumption. + - apply step_under_context with (K := AbsL Hole t2). assumption. + - apply step_under_context with (K := AbsR t1 Hole). assumption. + - apply step_under_context with (K := AppL Hole t2). assumption. + - apply step_under_context with (K := AppR t1 Hole). assumption. + - rename H0 into e. destruct t1; try discriminate. inversion e; subst; clear e. + apply ctx_red with (K := Hole). constructor. +Qed. + +Lemma next_step_none {n} {t: term n} : next_step t = None -> forall t', ¬ (t ≻ t'). +Proof. + induction t; simpl in *; intros e t'. + - apply no_var_step. + - destruct (next_step t1); try discriminate. destruct (next_step t2); try discriminate. + specialize (IHt1 eq_refl). specialize (IHt2 eq_refl). + intro H. apply pi_step in H. firstorder. + - destruct (next_step t1); try discriminate. destruct (next_step t2); try discriminate. + specialize (IHt1 eq_refl). specialize (IHt2 eq_refl). + intro H. apply abs_step in H. firstorder. + - destruct (next_step t1); try discriminate. destruct (next_step t2); try discriminate. + specialize (IHt1 eq_refl). specialize (IHt2 eq_refl). + intro H. inversion H; subst. destruct K; simpl in *; try discriminate. + + subst. inversion H1; subst; discriminate. + + inversion H0; subst. eapply IHt1. constructor. eassumption. + + inversion H0; subst. eapply IHt2. constructor. eassumption. + - apply no_srt_step. +Qed. + +Fixpoint normalize {n} (t: term n) (H: SN t) : term n := + match H with + | SN_on _ H => + match next_step t as o return next_step t = o -> term n with + | Some t' => fun e => normalize t' (H t' (next_step_some e)) + | None => fun _ => t + end eq_refl + end. + +Fixpoint step_star_normalize {n} (t: term n) (H: SN t) : t ≻* normalize t H. +Proof. + destruct H. simpl. + generalize (@eq_refl _ (next_step t)). + generalize (next_step t) at 2 3. + destruct o. + - intro. eapply Rstar_trans; swap 1 2. + + apply step_star_normalize. + + do 2 constructor. apply next_step_some. assumption. + - constructor. +Qed. + +Fixpoint normalize_normal_form {n} (t t': term n) (H: SN t) : ¬ normalize t H ≻ t'. +Proof. + destruct H. simpl. generalize (@eq_refl _ (next_step t)). generalize (next_step t) at 2 3. + destruct o. + - intro. apply normalize_normal_form. + - intro. apply next_step_none. assumption. +Qed. + +Lemma all_step_star_normalize {n} (t t': term n) (H: SN t) : t ≻* t' -> t' ≻* normalize t H. +Proof. + intro rleft. pose proof (rright := step_star_normalize t H). + destruct (confluence_step rleft rright) as [v [Hres rnorm]]. + enough (v = normalize t H) by (subst; assumption). destruct rnorm as [|? rnorm]; auto. + exfalso. revert rnorm. clear. induction 1; eauto using normalize_normal_form. + eapply normalize_normal_form; eassumption. +Qed. + +Lemma equiv_same_normal_form {n} (t t': term n) (H: SN t) (H' : SN t') : + t ≅ t' -> normalize t H = normalize t' H'. + intro Hcong. apply equiv_both_star in Hcong as [v [rt rt']]. + assert (rt't : t' ≻* normalize t H). + - eapply Rstar_trans; try eassumption. eapply all_step_star_normalize. assumption. + - apply all_step_star_normalize with (H := H') in rt't as [|? rnorm]; auto. + exfalso. revert rnorm. clear. induction 1; eauto. eapply normalize_normal_form; eassumption. +Qed. + +Fixpoint term_eqb {n} (t t' : term n) : bool := + match t, t' with + | Var k, Var k' => Nat.eqb (proj1_sig k) (proj1_sig k') + | Abs A t, Abs B u => term_eqb A B && term_eqb t u + | Srt Star, Srt Star | Srt Box, Srt Box => true + | Pi A B, Pi A' B' => term_eqb A A' && term_eqb B B' + | App t u, App t' u' => term_eqb t t' && term_eqb u u' + | _, _ => false + end. + +Lemma term_eqb_true_iff {n} (t t': term n) : term_eqb t t' = true <-> t = t'. +Proof. + split. + - induction t in t' |- *; destruct t'; simpl; + do 2 match goal with |- match ?s with _ => _ end = _ -> _ => destruct s | _ => idtac end; + try discriminate; try reflexivity; intro e; try apply andb_prop in e; f_equal; + intuition auto. + apply sig_lt_ext. apply Nat.eqb_eq. assumption. + - induction t in t' |- *; destruct t'; simpl; inversion 1; subst; + do 2 match goal with |- match ?s with _ => _ end = _ => destruct s | _ => idtac end; + try specialize (IHt1 _ eq_refl); try specialize (IHt2 _ eq_refl); eauto using andb_true_intro. + apply Nat.eqb_refl. +Qed. + +Lemma term_eqb_true {n} (t t': term n) : term_eqb t t' = true -> t = t'. + apply term_eqb_true_iff. +Qed. + +Lemma term_eqb_false_iff {n} (t t': term n) : term_eqb t t' = false <-> t <> t'. +Proof. + split. + - intros H e. apply term_eqb_true_iff in e. congruence. + - intros H. destruct (term_eqb _ _) eqn : e; auto. apply term_eqb_true in e. tauto. +Qed. + +Lemma term_eqb_false {n} (t t': term n) : term_eqb t t' = false -> t <> t'. + apply term_eqb_false_iff. +Qed. + +Definition term_eq_dec {n} (t t': term n) : {t = t'} + {t <> t'}. + destruct (term_eqb t t') eqn: e. + - left. apply term_eqb_true. assumption. + - right. apply term_eqb_false. assumption. +Defined. + +Definition convertible {n} (t t': term n) (H: SN t) (H': SN t') : bool := + term_eqb (normalize t H) (normalize t' H'). + +Lemma convertible_true_iff {n} (t t': term n) (H: SN t) (H': SN t') : + convertible t t' H H' = true <-> t ≅ t'. +Proof. + split. + - intro e. apply term_eqb_true in e. eapply Requiv_trans. + + apply Requiv_clot_star. apply step_star_normalize. + + rewrite e. apply Requiv_clot_star_r. apply step_star_normalize. + - intro. apply term_eqb_true_iff. apply equiv_same_normal_form. assumption. +Qed. + +Lemma convertible_true {n} (t t': term n) (H: SN t) (H': SN t') : + convertible t t' H H' = true -> t ≅ t'. + apply convertible_true_iff. +Qed. + +Lemma convertible_false_iff {n} (t t': term n) (H: SN t) (H': SN t') : + convertible t t' H H' = false <-> ¬ t ≅ t'. +Proof. + split. + - intros e Heq. apply convertible_true_iff with (H := H) (H' := H') in Heq. congruence. + - intro. destruct (convertible _ _ _ _) eqn: e; try reflexivity. + apply convertible_true in e. tauto. +Qed. + +Lemma convertible_false {n} (t t': term n) (H: SN t) (H': SN t') : + convertible t t' H H' = false -> ¬ t ≅ t'. + apply convertible_false_iff. +Qed. + +Definition convertible_dec {n} (t t': term n) (H: SN t) (H': SN t') : {t ≅ t'} + {¬ t ≅ t'} := + (if convertible t t' H H' as b return convertible t t' H H' = b -> _ + then fun e => left (convertible_true _ _ _ _ e) + else fun e => right (convertible_false _ _ _ _ e) + ) eq_refl. + +Definition convertible_typed {Sc} {n} {Γ Γ'} {t t': term n} + (H : exists T, Γ ⊢(Sc) t : T) (H' : exists T', Γ' ⊢(Sc) t' : T') : + {t ≅ t'} + {¬ t ≅ t'} := + convertible_dec t t' + (let (T, H) := H in typing_SN _ _ _ H) + (let (T', H') := H' in typing_SN _ _ _ H'). diff --git a/theories/LambdaCube/whnf.v b/theories/LambdaCube/whnf.v index bddea35..42f5f27 100644 --- a/theories/LambdaCube/whnf.v +++ b/theories/LambdaCube/whnf.v @@ -330,6 +330,18 @@ Proof. - eapply neutral_app_step; try eassumption. Qed. +Lemma whnf_is_sort_type_or_never_will_be {n} {t: term n} : + whnf t -> + match t with Srt _ => True | _ => forall s, ¬ (t ≅ Srt s) end. +Proof. + destruct t; auto; intros H ? e; apply Requiv_sym, srt_equiv in e. + - apply var_star in e. discriminate. + - apply pi_star in e. firstorder discriminate. + - apply abs_star in e. firstorder discriminate. + - inversion_clear H. inversion_clear H0. apply neutral_app_step_star in e; auto. + firstorder discriminate. +Qed. + Lemma whnf_is_pi_type_or_never_will_be {n} {t: term n} : whnf t -> match t with Pi _ _ => True | _ => forall A B, ¬ (t ≅ Pi A B) end. From c7cdeecba25174e3cd92eff094a7bb99850fb0a2 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Mon, 15 Dec 2025 12:34:23 +0100 Subject: [PATCH 20/21] Failed attempt at proving normalization, unclear if salvageable --- theories/LambdaCube/SN.v | 608 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 608 insertions(+) diff --git a/theories/LambdaCube/SN.v b/theories/LambdaCube/SN.v index 276d81f..ef30f49 100644 --- a/theories/LambdaCube/SN.v +++ b/theories/LambdaCube/SN.v @@ -3,9 +3,617 @@ From Coq Require Import Arith Lia. From FormArith Require Import Base. From FormArith.LambdaCube Require Import Term Operational Typing. + Inductive SN {n : nat} (t : term n) : Prop := | SN_on : (∀ u, t ≻ u → SN u) → SN t. +(* The following is an attempt at formalizing the proof of normalization for CoC + which can be found in Gilles Dowek's "Proofs in Theories" notes *) + +Notation "'𝓟' X" := (X → Prop) + (at level 10, + left associativity). + +Definition elem {X : Type} (x : X) (S : 𝓟 X) : Prop := S x. + +Notation "x ∈ X" := (elem x X) + (at level 20, + no associativity). + +Definition tset := ∀ (n : nat), 𝓟 (term n). + +Definition sn : tset := λ n t, SN t. + +Definition pi_set (X : tset) (S : 𝓟 tset) := + λ n (t : term n), + SN t ∧ + ∀ ty bod tm Y, + tm ∈ (X n) → + Y ∈ S → + t ≻* Abs ty bod → + bind (bind_first tm) bod ∈ (Y n). + +Definition tset_equiv (X Y : tset) : Prop := + ∀ n t, X n t ↔ Y n t. + +Notation "X ≡ Y" := (tset_equiv X Y) + (at level 20, + no associativity + ). + +Lemma tset_equiv_refl {X : tset} : X ≡ X. +Proof. firstorder. Qed. + +Lemma tset_equiv_sym {X Y : tset} : X ≡ Y → Y ≡ X. +Proof. firstorder. Qed. + +Lemma tset_equiv_trans {X Y Z : tset} : X ≡ Y → Y ≡ Z → X ≡ Z. +Proof. + intros XY YZ n t. + split. + - intros Xt. + apply YZ, XY, Xt. + - intros Zt. + apply XY, YZ, Zt. +Qed. + +Definition inter (S : 𝓟 tset) : tset := + λ n t, ∀ Y, Y ∈ S → Y n t. + +Notation "⋂ S" := (inter S) + (at level 10, + left associativity). + +Inductive candidate : tset → Prop := +| c_sn X : X ≡ sn → candidate X +| c_pi X S Z : Z ≡ pi_set X S → + candidate X → + (∀ Y, Y ∈ S → candidate Y) → + candidate Z +| c_inter X S : X ≡ ⋂ S → + (∀ Y, Y ∈ S → candidate Y) → + candidate X. + +Definition Cand : Prop := ∃ X, candidate X. + +Definition cand_sn : Cand := ex_intro _ _ (c_sn _ tset_equiv_refl). + +Inductive annot : Type := +| sing : annot +| c : annot +| func : annot → annot → annot. + +Lemma dec_eq_annot (x y : annot) : {x = y} + {x ≠ y}. +Proof. + induction x in y |-*. + - destruct y; [now left| right; discriminate..]. + - destruct y; [| now left |]; right; discriminate. + - destruct y; [right; discriminate..|]. + destruct (IHx1 y1) as [-> | H]. + + destruct (IHx2 y2) as [-> | H]; [now left|]. + right. + now injection. + + right. + now injection. +Qed. + +Lemma annot_UIP {x y : annot} (p q : x = y) : p = q. +Proof. + apply Eqdep_dec.UIP_dec, dec_eq_annot. +Qed. + +Fixpoint M_annot {n} (t : term n) : annot := + match t with + | Srt _ => c + | Var _ => sing + | Abs _ t => M_annot t + | App t _ => M_annot t + | Pi ty fam => + match M_annot fam with + | sing => sing + | ann_f => + match M_annot ty with + | sing => ann_f + | ann_ty => func ann_ty ann_f + end + end + end. + +Fixpoint M_annot_ctx {m n} (K : ctx m n) (a : annot) : annot := + match K with + | Hole => a + | AbsL _ t => M_annot t + | AbsR _ K => M_annot_ctx K a + | AppL K _ => M_annot_ctx K a + | AppR t _ => M_annot t + | PiL K fam => + match M_annot fam with + | sing => sing + | ann_f => + match M_annot_ctx K a with + | sing => ann_f + | ann_ty => func ann_ty ann_f + end + end + | PiR ty K => + match M_annot_ctx K a with + | sing => sing + | ann_f => + match M_annot ty with + | sing => ann_f + | ann_ty => func ann_ty ann_f + end + end + end. + +Fixpoint ann_interp (ann : annot) : Prop := + match ann with + | c => Cand + | sing => True + | func ann_b ann_f => ann_interp ann_b → ann_interp ann_f + end. + +Definition M {n} (t : term n) : Prop := ann_interp (M_annot t). + +Lemma M_annot_fill {m n} (t : term m) (K : ctx m n) : + M_annot (fill K t) = M_annot_ctx K (M_annot t). +Proof. + induction K; auto; + simpl; + now rewrite IHK. +Qed. + +Lemma M_annot_object {Sc n} (Γ : typing_ctx n) (t A : term n) : + Γ ⊢(Sc) A : Srt Star → Γ ⊢(Sc) t : A → M_annot t = sing. +Proof. + induction 2; subst. + - contradict H. + clear. + remember (Srt Box). + induction 1; try discriminate; tauto. + - reflexivity. + - contradict H. + clear. + destruct s'; swap 1 2. + { remember (Srt Box). + induction 1; try discriminate; tauto. + } + intros C. + apply typ_star_inv in C. + apply srt_equiv_srt in C. + discriminate. + - simpl. + apply IHtyping3. + apply typ_pi_inv in H as (s1 & s2 & eq_star2 & typ_A & typ_B & pi_sc). + apply srt_equiv_srt in eq_star2. + subst. + assumption. + - simpl. + apply IHtyping1. + apply srt_typing in H0_ as [|[s' typ_piAB]]; [discriminate|]. + apply typ_pi_inv in typ_piAB as (s1 & s2 & eq_star2 & typ_A & typ_B & pi_sc). + destruct s2; try solve [econstructor; eauto]. + pose proof (bind_first_typ H0_0 typ_B) as typ_B'. + simpl in typ_B'. + pose proof (unique_typing H typ_B'). + apply srt_equiv_srt in H0. + discriminate. + - apply IHtyping1. + apply srt_typing in H0_ as [C | [s' typ_C]]. + + subst. + apply srt_equiv in H0. + pose proof (subject_reduction _ _ _ _ _ H H0) as C'. + contradict C'. + clear. + remember (Srt Box). + induction 1; try discriminate; tauto. + + destruct s'; [assumption|]. + apply equiv_both_star in H0 as (v & red_A & red_B). + pose proof (subject_reduction _ _ _ _ _ typ_C red_A) as Hv1. + pose proof (subject_reduction _ _ _ _ _ H red_B) as Hv2. + pose proof (unique_typing Hv1 Hv2) as C''. + apply srt_equiv_srt in C''. + discriminate. +Qed. + +Lemma M_annot_type {Sc n} (Γ : typing_ctx n) (A B : term n) : + Γ ⊢(Sc) B : Srt Box → + Γ ⊢(Sc) A : B → M_annot A = sing. +Proof. + induction 2; subst; try discriminate. + - contradict H. + clear. + generalize (Srt (n := n) Box) at 2. + intros B. + remember (Srt Box). + induction 1; try discriminate; tauto. + - reflexivity. + - destruct s'; swap 1 2. + { contradict H. + clear. + generalize (Srt (n := n) Box) at 2. + intros B. + remember (Srt Box). + induction 1; try discriminate; tauto. + } + simpl. + rewrite IHtyping2; [reflexivity|]. + constructor. + eapply typing_imp_ctx_wf. + eassumption. + - simpl. + apply IHtyping3. + apply typ_pi_inv in H as (s1 & s2 & eq_star2 & typ_A & typ_B & pi_sc). + apply srt_equiv_srt in eq_star2 as <-. + assumption. + - simpl. + apply IHtyping1. + apply srt_typing in H0_ as [|[s typ_B]]; [discriminate|]. + apply typ_pi_inv in typ_B as (s1 & s2 & eq_star2 & typ_A & typ_B & pi_sc). + clear dependent s. + enough (s2 = Box). + + subst. + econstructor; eassumption. + + eapply srt_equiv_srt, unique_typing; [|eassumption]. + eapply (bind_first_typ (T := Srt s2)); eassumption. + - apply IHtyping1. + apply srt_typing in H0_ as [C | [s' typ_C]]. + + subst. + apply srt_equiv in H0. + pose proof (subject_reduction _ _ _ _ _ H H0) as C'. + contradict C'. + clear. + generalize (Srt (n := n) Box) at 2. + intros B. + remember (Srt Box). + induction 1; try discriminate; tauto. + + destruct s'; [|assumption]. + apply equiv_both_star in H0 as (v & red_A & red_B). + pose proof (subject_reduction _ _ _ _ _ typ_C red_A) as Hv1. + pose proof (subject_reduction _ _ _ _ _ H red_B) as Hv2. + pose proof (unique_typing Hv1 Hv2) as C''. + apply srt_equiv_srt in C''. + discriminate. +Qed. + +Lemma M_annot_typ_srt {Sc n} (Γ : typing_ctx n) (t A : term n) (s : sort): + Γ ⊢(Sc) A : Srt s → + Γ ⊢(Sc) t : A → M_annot t = sing. +Proof. + destruct s. + - apply M_annot_object. + - apply M_annot_type. +Qed. + +Lemma M_annot_ren {m} (t : term m) : + ∀ n (σ : {i | i < m} → {i | i < n}), + M_annot (ren σ t) = M_annot t. +Proof. + induction t; simpl; trivial. + intros k σ. + rewrite IHt1, IHt2. + reflexivity. +Qed. + +Lemma M_annot_bind {m} (t : term m) : + ∀ n (σ : {i | i < m} → term n), + (∀ i, M_annot (σ i) = sing) → + M_annot (bind σ t) = M_annot t. +Proof. + induction t. + - simpl. auto. + - intros. + simpl. + rewrite IHt1, IHt2; trivial. + intros i. + unfold lift_bind. + destruct (lt_dec _ _). + + simpl. + now rewrite M_annot_ren. + + reflexivity. + - intros. + simpl. + apply IHt2. + unfold lift_bind. + intros. + destruct (lt_dec _ _). + + simpl. + now rewrite M_annot_ren. + + reflexivity. + - simpl. assumption. + - trivial. +Qed. + +Lemma M_annot_head_step {Sc n} (Γ : typing_ctx n) (t u A B : term n) : + Γ ⊢(Sc) t : A → + t [≻] u → + M_annot t = M_annot u. +Proof. + intros typ_t t_red. + destruct t_red. + simpl. + apply typ_app_inv in typ_t as (C & D & A_eq_B & typ_abs & typ_arg). + apply typ_abs_inv in typ_abs as (s1 & s2 & E & F & pi_eq & typ_ty & typ_E & typ_body & typ_pi & pi_sc). + apply pi_equiv_pi in pi_eq as [C_eq D_eq]. + apply typ_pi_inv in typ_pi as (s3 & s4 & srt_eq & typ_C & typ_D & pi_sc'). + symmetry. + apply M_annot_bind. + intros i. + unfold bind_first. + destruct (lt_dec _ _); [reflexivity|]. + eapply M_annot_typ_srt; eassumption. +Qed. + +Lemma M_annot_step {Sc n} (Γ : typing_ctx n) (t u A B : term n) : + Γ ⊢(Sc) t : A → + t ≻ u → + M_annot t = M_annot u. +Proof. + intros typ_t red_t. + revert typ_t. + destruct red_t as [m K t' u' red_t']. + intros typ_Kt'. + rewrite !M_annot_fill. + f_equal. + apply typed_imp_subterm_typed in typ_Kt' as (Γ' & A' & typ_t'). + eapply M_annot_head_step; eassumption. +Qed. + +Lemma M_annot_red_plus {Sc n} (Γ : typing_ctx n) (t u A B : term n) : + Γ ⊢(Sc) t : A → + t ≻+ u → + M_annot t = M_annot u. +Proof. + intros typ_t red_t. + induction red_t. + - rewrite IHred_t. + eapply M_annot_step; try eassumption. + eapply subject_reduction; [|apply Rclot_plus_star; eassumption]. + eassumption. + - eapply M_annot_step; eassumption. +Qed. + +Lemma M_annot_red {Sc n} (Γ : typing_ctx n) (t u A B : term n) : + Γ ⊢(Sc) t : A → + t ≻* u → + M_annot t = M_annot u. +Proof. + intros typ_t red_t. + destruct red_t. + - reflexivity. + - eapply M_annot_red_plus; eassumption. +Qed. + +Lemma M_annot_equiv {Sc n} (Γ Δ : typing_ctx n) (t u A B : term n) : + Γ ⊢(Sc) t : A → + Δ ⊢(Sc) u : B → + t ≅ u → + M_annot t = M_annot u. +Proof. + intros typ_t typ_u t_eq_u. + apply equiv_both_star in t_eq_u as (v & red_t & red_u). + transitivity (M_annot v); + [|symmetry]; + eapply M_annot_red; + eassumption. +Qed. + +Lemma M_equiv {Sc n} (Γ Δ : typing_ctx n) (t u A B : term n) : + Γ ⊢(Sc) t : A → + Δ ⊢(Sc) u : B → + t ≅ u → + M t = M u. +Proof. + intros. + unfold M. + f_equal. + eapply M_annot_equiv; + eassumption. +Qed. + +Definition val (Sc : pi_scheme) {n} (Γ : typing_ctx n) := + ∀ (i : nat) (H : i < n), M (kth_index_ctx Γ i H). + +Definition extend {Sc n} {Γ : typing_ctx n} {A} (Φ : val Sc Γ) (a : M A) : val Sc (Γ; A). +Proof. + intros i H. + simpl kth_index_ctx. + unfold M. rewrite M_annot_ren. + destruct (lt_dec i n) as [H1 | H1]. + - apply Φ. + - assumption. +Defined. + +Fixpoint denot + Sc {n} (Γ : typing_ctx n) + (t A : term n) (H : Γ ⊢(Sc) t : A) + (Φ : val Sc Γ) {struct t} + : M A. +Proof. + destruct t. + - apply typ_var_inv in H as A_eq_kth. + assert (e : M_annot A = M_annot (kth_index_ctx Γ (proj1_sig s) (proj2_sig s))). + { + apply srt_typing in H as typ_A. + apply typing_imp_ctx_wf in H. + destruct typ_A as [contra|[s' typ_A]]. + + subst. + apply srt_equiv in A_eq_kth. + epose proof (wf_ctx_contains_types H) as [s' typ_kth]. + eapply subject_reduction in typ_kth; [|eassumption]. + contradict typ_kth. + clear. + remember (Srt Box) as B. + induction 1; try discriminate; tauto. + + epose proof (wf_ctx_contains_types H) as [s'' typ_kth]. + eapply M_annot_equiv; try eassumption. + } + unfold M. + rewrite e. + apply Φ. + - apply typ_pi_inv in H as H1. + destruct H1 as (s & s' & A_eq_s' & typ_t1 & typ_t2 & psc). + assert (M_annot A = c). + { + destruct s'. + - apply srt_typing in H as [contra|typ_A]. + { subst. + now apply srt_equiv_srt in A_eq_s'. + } + destruct typ_A as [s0 typ_A]. + unshelve erewrite (M_annot_equiv _ _ _ _ _ _ _ ltac:(constructor) A_eq_s'). + 5 : eassumption. + 1 : assumption. + { eapply typing_imp_ctx_wf. eassumption. } + reflexivity. + - apply Requiv_sym, srt_equiv in A_eq_s'. + apply srt_typing in H as [|[s0 typ_A]]; [now subst|]. + pose proof (subject_reduction _ _ _ _ _ typ_A A_eq_s') as C'. + contradict C'. + clear. + remember (Srt Box). + induction 1; try discriminate; tauto. + } + unfold M. + rewrite H0. + set (X := denot _ _ _ _ _ typ_t1 Φ). + destruct X as [X cX]. + set (S := λ (Y : tset), ∃ c H, ex_intro _ Y H = denot Sc _ _ t2 _ typ_t2 (extend Φ c)). + econstructor. + unshelve eapply (c_pi _ S _ _ cX). + { apply tset_equiv_refl. } + intros Y HY. + unfold S, elem in HY. + now destruct HY as (c & cY & Y_eq). + - apply typ_abs_inv in H as H1. + destruct H1 as (s & s' & B & X & A_eq & typ_t1 & typ_B & typ_t2 & typ_1 & psc). + unfold M. + unshelve erewrite (M_annot_equiv _ Γ _ _ _ _ typ_1 _ A_eq). + 2 : {econstructor; eassumption. } + simpl. + assert (M_annot B = sing ∨ M_annot B ≠ sing) as [-> | ann_B]. + { + destruct (M_annot B); [now left|right..]; discriminate. + } + { now simpl. } + assert (M_annot t1 = sing ∨ M_annot t1 ≠ sing) as [ann_t1 | ann_t1]. + { + destruct (M_annot t1); [now left|right..]; discriminate. + } + { + assert (e : M t1). + { + unfold M. + rewrite ann_t1. + now simpl. + } + rewrite ann_t1. + pose proof (v := denot _ _ _ _ _ typ_t2 (extend Φ e)). + unfold M in v. + now destruct (M_annot B) eqn:ann_B'. + } + pose proof (λ x, denot _ _ _ _ _ typ_t2 (extend Φ x)) as f. + unfold M in f. + destruct (M_annot B), (M_annot t1); try contradiction; assumption. + - apply typ_app_inv in H as H1. + destruct H1 as (A0 & B & A_eq & typ_t1 & typ_t2). + apply srt_typing in typ_t1 as H2. + destruct H2 as [|[s0 H2]]; [discriminate|]. + apply typ_pi_inv in H2 as H3. + destruct H3 as (s & s' & srt_eq & typ_A0 & typ_B & psc). + apply srt_equiv_srt in srt_eq as ->. + assert (M_annot t2 = sing). + { + eapply M_annot_typ_srt; eassumption. + } + unfold M. + replace (M_annot A) with (M_annot B); swap 1 2. + { + apply srt_typing in H as [-> | [s0 H1]]. + { eapply srt_equiv, subject_reduction in A_eq; swap 1 2. + - eapply bind_first_typ; eassumption. + - simpl in A_eq. + contradict A_eq. + clear. + remember (Srt Box). + induction 1; try discriminate; tauto. + } + unshelve erewrite (M_annot_equiv _ _ _ _ _ _ _ _ A_eq). + 7 : { eapply bind_first_typ; eassumption. } + 3 : { apply H1. } + symmetry. + apply M_annot_bind. + intros i. + unfold bind_first. + now destruct (lt_dec _ _). + } + pose proof (denot _ _ _ _ _ typ_t1 Φ) as f. + pose proof (denot _ _ _ _ _ typ_t2 Φ) as x. + unfold M in f, x. + simpl in f. + assert (M_annot B = sing ∨ M_annot B ≠ sing) as [-> | ann_B]. + { + destruct (M_annot B); [now left|right..]; discriminate. + } + { now simpl. } + assert (M_annot A0 = sing ∨ M_annot A0 ≠ sing) as [ann_A0 | ann_A0]. + { + destruct (M_annot A0); [now left|right..]; discriminate. + } + { rewrite ann_A0 in *. + now destruct (M_annot B). + } + destruct (M_annot A0), (M_annot B); try contradiction; exact (f x). + - destruct s. + + apply srt_typing in H as H1. + destruct H1 as [->|contra]. + { exact cand_sn. } + destruct contra as [s0 H1]. + apply typ_star_inv, Requiv_sym, srt_equiv in H. + eapply subject_reduction in H1; [|eassumption]. + contradict H1. + clear. + remember (Srt Box). + induction 1; try discriminate; tauto. + + contradict H. + clear. + remember (Srt Box). + induction 1; try discriminate; tauto. +Defined. + +Lemma denot_irrel + Sc {n} (Γ : typing_ctx n) + (t A : term n) (H1 H2 : Γ ⊢(Sc) t : A) + (Φ : val Sc Γ) : denot _ _ _ _ H1 Φ = denot _ _ _ _ H2 Φ. +Proof. + induction t; simpl. + - f_equal. + apply annot_UIP. + - destruct (typ_pi_inv _ _ _ _ _), (typ_pi_inv _ _ _ _ _). + destruct e, e0. + destruct a, a0. + destruct a, a0. + destruct a, a0. + f_equal. + + assert (x = x0) as q. + { + eapply srt_equiv_srt, unique_typing; eassumption. + } + destruct q. + assert (x1 = x2) as q. + { + eapply srt_equiv_srt, unique_typing; eassumption. + } + destruct q. + rewrite (IHt1 _ _ t t0). + destruct (denot _ _ _ _ _). + unshelve eapply eq_ex_intro. + * f_equal. + (* Unfortunately this requires funext, stating a + precise equivalence lemma might be too involved*) +Abort. + + Lemma typing_SN {Sc : pi_scheme} {n : nat} (Γ : typing_ctx n) (t A : term n) : Γ ⊢(Sc) t : A → SN t. Admitted. From 7312b4442d53e1d36852601dece1d44fd6affd8a Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Mon, 15 Dec 2025 12:41:38 +0100 Subject: [PATCH 21/21] Renamed files --- theories/LambdaCube/{infer.v => Infer.v} | 2 +- theories/LambdaCube/{normalize.v => Normalize.v} | 2 +- theories/LambdaCube/{whnf.v => WHNF.v} | 0 3 files changed, 2 insertions(+), 2 deletions(-) rename theories/LambdaCube/{infer.v => Infer.v} (99%) rename theories/LambdaCube/{normalize.v => Normalize.v} (99%) rename theories/LambdaCube/{whnf.v => WHNF.v} (100%) diff --git a/theories/LambdaCube/infer.v b/theories/LambdaCube/Infer.v similarity index 99% rename from theories/LambdaCube/infer.v rename to theories/LambdaCube/Infer.v index 56d15f5..c974e01 100644 --- a/theories/LambdaCube/infer.v +++ b/theories/LambdaCube/Infer.v @@ -1,7 +1,7 @@ From Coq Require Import Utf8. From Coq Require Import Arith Lia. From FormArith Require Import Base. -From FormArith.LambdaCube Require Import Term Operational Typing SN whnf normalize. +From FormArith.LambdaCube Require Import Term Operational Typing SN WHNF Normalize. Inductive strong_ctx_wf (Sc: pi_scheme) : forall {n}, typing_ctx n -> Type := | strong_empty_wf : strong_ctx_wf Sc \ diff --git a/theories/LambdaCube/normalize.v b/theories/LambdaCube/Normalize.v similarity index 99% rename from theories/LambdaCube/normalize.v rename to theories/LambdaCube/Normalize.v index 0393d62..7cbfc27 100644 --- a/theories/LambdaCube/normalize.v +++ b/theories/LambdaCube/Normalize.v @@ -1,7 +1,7 @@ From Coq Require Import Utf8. From Coq Require Import Arith Lia. From FormArith Require Import Base. -From FormArith.LambdaCube Require Import Term Operational Typing SN whnf. +From FormArith.LambdaCube Require Import Term Operational Typing SN WHNF. Fixpoint next_step {n} (t: term n) : option (term n) := match t with diff --git a/theories/LambdaCube/whnf.v b/theories/LambdaCube/WHNF.v similarity index 100% rename from theories/LambdaCube/whnf.v rename to theories/LambdaCube/WHNF.v