Comparing 5ea75052a5...5a7f46a8a1 - yiyunliu/sp-eta-postpone - Forgejo: Write more proofs and functional programs.

yiyunliu/sp-eta-postpone

Sign in to create a new pull request.

Author	SHA1	Message	Date
Yiyun Liu	5a7f46a8a1	Finish the enhanced eta postponement	2025-01-30 23:29:25 -05:00
Yiyun Liu	51ac5ffbd6	Finish eta postponement	2025-01-30 23:10:11 -05:00
Yiyun Liu	9134cfec8a	Finish a few cases of eta postponement	2025-01-30 22:18:58 -05:00
Yiyun Liu	d925a8bcaa	Minor cleanup	2025-01-30 20:23:57 -05:00
Yiyun Liu	fc666956e2	Finish off the SN proof	2025-01-30 20:23:25 -05:00
Yiyun Liu	64e558f09e	Finish sn unsubst	2025-01-30 20:17:00 -05:00
Yiyun Liu	c83be03230	Finish antirenaming	2025-01-30 16:14:56 -05:00
Yiyun Liu	e4c2bd39db	Finish the eta split proof without any admits	2025-01-29 23:41:38 -05:00
Yiyun Liu	20eef78014	Finish one example case of violate sn	2025-01-29 22:59:57 -05:00
Yiyun Liu	aa2c2ca151	Add lemmas that bad forms are impossible	2025-01-29 22:25:14 -05:00
Yiyun Liu	a47d69f427	More no forbid	2025-01-29 22:19:36 -05:00
Yiyun Liu	99b5e87ea3	Finish red sn preservation	2025-01-29 22:09:08 -05:00
Yiyun Liu	369bd55932	Add red sn preservation	2025-01-29 21:27:49 -05:00
Yiyun Liu	5f619c0980	Finish the split lemma up to strong normalization	2025-01-29 15:52:05 -05:00
Yiyun Liu	710b59fd8f	Prove all application cases	2025-01-29 14:01:35 -05:00
Yiyun Liu	08b9395acb	Push some important cases of the split lemma	2025-01-29 13:37:54 -05:00
Yiyun Liu	3f3703990d	Save progress	2025-01-28 16:37:23 -05:00
Yiyun Liu	24693b8928	Add "beta-free" eta contraction	2025-01-28 16:07:52 -05:00
Yiyun Liu	61e743ee74	Add ne ered	2025-01-28 15:14:33 -05:00

1 changed files with 750 additions and 342 deletions

1092

theories/fp_red.v

View file

File diff suppressed because it is too large Load diff