Commit graph

84 commits

Author SHA1 Message Date
4fde2442f1 fix naming of rules in expr_lc 2024-09-24 04:42:45 +02:00
a5d8cb979b rename context to env 2024-09-24 04:42:45 +02:00
cc96cee283
add environment library to metatheory 2024-09-24 04:41:56 +02:00
d690d6dcdc
organize coq sources in subdirectories 2024-09-21 13:00:57 +02:00
30fe571a39
open scopes locally 2024-09-21 12:33:10 +02:00
6f3b0fbc0b
typing: use cofinite quantification 2024-09-21 06:48:26 +02:00
67e4c13d57
translate morphism path: fix morph mapping 2024-09-21 06:47:55 +02:00
3c86dde677
improve notation for opening/substitution & add proof for expr_subst_fresh 2024-09-21 01:43:25 +02:00
4b76d6a982
improve type-opening lemmas 2024-09-21 01:05:28 +02:00
f8effc45ad add evaluation for debruijn terms 2024-09-21 00:41:45 +02:00
8b19caa9f2 add substitution & opening fixpoints for expressions 2024-09-21 00:41:45 +02:00
3c5859b43c add translate_typing for debruijn terms 2024-09-21 00:41:45 +02:00
1edbb8d748 add context, morphism translation & typing for debruijn terms 2024-09-21 00:41:45 +02:00
f76cec4a9d add subtype relations for debruijn terms 2024-09-21 00:41:45 +02:00
377f57e124 equiv_debruijn: add more hints & simplify TEq_Symm proof 2024-09-21 00:41:45 +02:00
1d6fb9ab6d add equivalence relation for debruijn types 2024-09-21 00:41:45 +02:00
f174eb1061 add notation for debruijn terms 2024-09-21 00:41:45 +02:00
c4f4e56fee move subst/opening lemmas to separate file 2024-09-21 00:41:45 +02:00
b97cb84caf use 'atom' in debruijn terms & complete proofs about type subst / open 2024-09-21 00:41:45 +02:00
9264d28837 take over Metatheory, FiniteSet & Atom libraries from popl-tutorial 2024-09-21 00:41:40 +02:00
bd3504614b
popl-tutorial Fsub: sanitize base libraries
mostly add Admitted everywhere
2024-09-19 21:13:59 +02:00
6773f81ff5
initial beamer 2024-09-19 14:17:48 +02:00
fd2c035902
work on soundness proofs & fix bug in translate_typing 2024-09-19 07:02:27 +02:00
dbfe0cf4de
add initial impl of debruijn terms 2024-09-19 01:48:12 +02:00
826077e37b
coq: add translate_typing example
& other minor stuff
2024-09-19 01:46:29 +02:00
d23ad61ba3
coq: type equiv: add subfun/submorph 2024-09-19 01:41:51 +02:00
6e5c832db7
add notation for sequence types & use notations everywhere 2024-09-18 11:15:20 +02:00
633843d9c7
work on abstract & intro 2024-09-17 18:36:38 +02:00
127debf945
terms notation: add ident rule to allow variables in notation instance 2024-09-17 03:14:49 +02:00
f53f226f55
remove module wraps in each file 2024-09-17 03:13:36 +02:00
05c137c489
import implementation of Fsub from the Coq tutorial of UPenn
taken from 'https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/index.html'
2024-09-16 17:58:18 +02:00
44d8d401d8
adapt eval relation & add reduction example
add expr_descend Notation [{ e des τ }]
2024-09-16 17:54:32 +02:00
12da3e97bd
change meaning of expr_ascend to only explicitly state the top segment of the type ladder.
also add associativity of ladder types in type-equivalence
2024-09-16 15:58:29 +02:00
cae0572e1b
wip on preservation proof 2024-09-16 15:14:53 +02:00
638ddf4fd1
coq: add translate_typing 2024-09-08 15:34:15 +02:00
10ca08c5a0
coq typing relation: add DescendImplicit rule in addition to Descend rule for explicit type-downcasts
add one more typing example
2024-09-08 15:33:54 +02:00
4b3358372e
coq: typing relation fix ctx assignments in premisse 2024-09-08 15:32:54 +02:00
b44e443879
add translate_morphism_path \& morphism path examples 2024-09-08 15:30:09 +02:00
850285cff0
morphism paths: add Lift path 2024-09-08 15:29:47 +02:00
865ceff7d4
add remaining notations for expr_term 2024-09-08 15:28:44 +02:00
c3d1649402
expr term: remove explicit variable-type from expr_let 2024-09-08 14:48:36 +02:00
bf7846294f
coq: move context into separate module, define morphism-path & redefine typing rules 2024-09-05 12:47:30 +02:00
e62c028126
paper: adapt soundness theorems 2024-09-05 12:46:24 +02:00
6f81686105
paper: define morphism-path relation, redefine typing-relation \& translation 2024-09-05 11:20:21 +02:00
2d557e51e4
WIP coq: debruijn terms 2024-09-04 12:47:03 +02:00
d1742c51d5
coq: remove delta_step definition 2024-09-04 12:46:37 +02:00
1bd55cd8c3
paper: rename inference rules to match coq definitions 2024-09-04 12:45:33 +02:00
fd8ca35a27
paper: add new coq files to appendix 2024-09-04 12:44:24 +02:00
b31c8abc6c
initial definition of soundness theorems 2024-09-04 12:41:17 +02:00
2db774ae68
initial definition of expand_morphisms 2024-09-04 12:41:00 +02:00