Merge the prop equality extension #287

Ailrun · 2025-06-19T19:53:50Z

Closes #181

merge

* update syntax for propositional equality * empty * do not extract * don't build dune * do not run test * update comments

* add rules for prop equality * bring back more files * bad naming * not enough premises

Port updates from the main branch

Port Fix weird TOC (#215)

…rammar

Merge main for grammar fix

* fixing presupposition * working on presup * need to figure this out * update * one more case * one more lemma * I am so dead... * move out lemmas * more progress * finish one lemma * long way to go * outline the proof * outline the proof * one simple case * keep completing * more proofs * the most complicated case * more proofs * more proofs * more proofs * finish proofs * add presup * finish all syntactic proofs

…q-presup

Update prop eq presup

Update CI to have (temporary) extension page

Port consistency

Port notation

Optimize presup a bit

* Update ci_build.yaml (#242) * Simplify installation steps (#243)

Optimize a bit more

Port main

backward merge

* Restore Semantics * Add Completeness placeholders * Add missing file * Reflect comments

* Completeness is complex * Something is wrong with PER model * Something * Some progress on completeness * Finish easy cases

* need to define mutual versions of lemmas * fill in the lemma * more proofs * one more case * proved a lemma * update lemmas * one more lemma * typos

Ailrun · 2025-06-20T08:53:32Z

Equality cases for the soundness is also a bit optimized (by a fairly naive method) and now it takes 2/3 compile time.
Basically, there were some redundant mautos after transitivity when it does not remove neither of branch.
While optimizing it, I also made the proof structure clearer (so that there will be only one focused goal).

Port #288 to ext/prop-eq

jiangsy · 2025-06-27T13:33:19Z

Just to double check, though #288 is merged, there are still usage of UIP in this branch, right?

Ailrun · 2025-06-30T19:03:27Z

Yes, some new lemmas and the equality cases should be fixed.

jiangsy · 2025-06-30T19:05:00Z

Sure, after we merge #290, we would (hopefully) see how many things need fix

jiangsy · 2025-06-30T20:00:00Z

Unexpected axiom usage:
{'Eqdep.Eq_rect_eq.eq_rect_eq'}

Detailed usage:
('Algorithmic/Subtyping/Lemmas.v - alg_subtyping_complete', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Subtyping/Lemmas.v - alg_subtyping_sound', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_sound', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_check_sound', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_infer_sound', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_infer_normal', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_check_typ_implies_alg_type_infer_typ', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_check_pi_implies_alg_type_infer_pi', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_check_subtyp', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_check_conv', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_check_complete', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_infer_complete', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_infer_typ_complete', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Algorithmic/Typing/Lemmas.v - alg_type_infer_pi_complete', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/Consequences/Rules.v - ctxeq_nbe_eq', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Core/Completeness/Consequences/Rules.v - ctxeq_nbe_eq'", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/Consequences/Rules.v - ctxeq_nbe_ty_eq', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Core/Completeness/Consequences/Rules.v - ctxeq_nbe_ty_eq'", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/Consequences/Types.v - exp_eq_typ_implies_eq_level', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/Consequences/Types.v - is_typ_constr_and_exp_eq_var_implies_eq_var', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/Consequences/Types.v - is_typ_constr_and_exp_eq_typ_implies_eq_typ', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/Consequences/Types.v - is_typ_constr_and_exp_eq_nat_implies_eq_nat', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/EqualityCases.v - rel_exp_eqrec_cong', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/FundamentalTheorem.v - completeness_fundamental', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/FundamentalTheorem.v - completeness_fundamental_ctx', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/FundamentalTheorem.v - completeness_fundamental_ctx_subtyp', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/FundamentalTheorem.v - completeness_fundamental_exp', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/FundamentalTheorem.v - completeness_fundamental_exp_eq', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/FundamentalTheorem.v - completeness_fundamental_sub', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/FundamentalTheorem.v - completeness_fundamental_sub_eq', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/FundamentalTheorem.v - completeness_fundamental_subtyp', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness/FundamentalTheorem.v - completeness_fundamental_ctx_eq', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness.v - completeness', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Completeness.v - completeness_ty', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - idempotent_nbe', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Core/Semantic/Consequences.v - idempotent_nbe'", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - idempotent_nbe_ty', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - adjust_exp_eq_level', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - exp_eq_pi_inversion', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - nf_of_pi', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - canonical_form_of_pi', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - canonical_form_of_nat', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - canonical_form_of_typ', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - subtyp_spec', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - consistency_ne_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Semantic/Consequences.v - consistency', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/ContextCases.v - glu_rel_ctx_extend', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/EqualityCases.v - glu_rel_eq', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/EqualityCases.v - glu_rel_eq_refl', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/EqualityCases.v - glu_rel_exp_eq_clean_inversion', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/EqualityCases.v - glu_rel_eq_eqrec', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/FunctionCases.v - glu_rel_exp_pi', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/FunctionCases.v - glu_rel_exp_fn_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/FunctionCases.v - glu_rel_exp_fn', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/FunctionCases.v - glu_rel_exp_app_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/FunctionCases.v - glu_rel_exp_app', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/FundamentalTheorem.v - soundness_fundamental', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/FundamentalTheorem.v - soundness_fundamental_ctx', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/FundamentalTheorem.v - soundness_fundamental_exp', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/FundamentalTheorem.v - soundness_fundamental_sub', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_ctx_env_per_ctx_env', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_ctx_env_resp_per_ctx_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - functional_glu_ctx_env', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_ctx_env_cons_clean_inversion', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_ctx_env_subtyp_sub_if', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_rel_exp_clean_inversion1', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_rel_exp_clean_inversion2', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_rel_exp_to_wf_exp', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Core/Soundness/LogicalRelation/Lemmas.v - glu_ctx_env_cons_clean_inversion'_helper", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Core/Soundness/LogicalRelation/Lemmas.v - glu_ctx_env_cons_clean_inversion'", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_rel_sub_clean_inversion1', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_rel_sub_clean_inversion2', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_rel_sub_clean_inversion3', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_rel_sub_wf_sub', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/LogicalRelation/Lemmas.v - glu_rel_exp_preserves_lvl', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - glu_rel_exp_sub_nat', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Core/Soundness/NatCases.v - glu_rel_exp_clean_inversion2''", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - glu_rel_exp_succ', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - glu_rel_sub_extend_nat', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - glu_rel_exp_natrec_zero_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - glu_rel_exp_natrec_succ_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - cons_glu_sub_pred_q_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - cons_glu_sub_pred_q_nat_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - glu_rel_exp_natrec_neut_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - glu_rel_exp_natrec_helper', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/NatCases.v - glu_rel_exp_natrec', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/SubstitutionCases.v - glu_rel_sub_compose', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/SubstitutionCases.v - glu_rel_sub_extend', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/SubtypingCases.v - glu_rel_exp_subtyp', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/SubtypingCases.v - glu_rel_sub_subtyp', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/SubtypingCases.v - glu_rel_exp_conv', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/SubtypingCases.v - glu_rel_sub_conv', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/TermStructureCases.v - glu_rel_exp_vlookup', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/TermStructureCases.v - glu_rel_exp_sub', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Core/Soundness/UniverseCases.v - glu_rel_exp_clean_inversion2'", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/UniverseCases.v - glu_rel_exp_sub_typ', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness/UniverseCases.v - glu_rel_exp_typ_sub_clean_inversion', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness.v - soundness', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Core/Soundness.v - soundness'", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Core/Soundness.v - soundness_ty', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Core/Soundness.v - soundness_ty'", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
("Extraction/TypeCheck.v - type_check_complete'", ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Extraction/TypeCheck.v - type_infer_complete', ['Eqdep.Eq_rect_eq.eq_rect_eq'])
('Extraction/TypeCheck.v - type_check_closed_complete', ['Eqdep.Eq_rect_eq.eq_rect_eq'])

Ailrun · 2025-06-30T21:44:37Z

so it's mostly soundness

jiangsy · 2025-06-30T21:58:33Z

seems like that, the only broken one in completeness is 'Core/Completeness/EqualityCases.v - rel_exp_eqrec_cong'

theories/Core/Completeness/LogicalRelation/Lemmas.v

HuStmpHrrr · 2025-07-07T06:20:28Z

it seems Clare has created a branch so I would say changes to main do not impact the artifact. we can release from the icfp25 branch. I would like this PR to be merged as a rebase to keep track of the changes along the way, but there is a conflict. can this be fixed easily?

Ailrun · 2025-07-07T08:03:09Z

I think for this one it would be better to make a merge commit (but not squash), as several backporting merge has already been done between this one and main.

HuStmpHrrr and others added 30 commits September 14, 2024 22:02

Merge pull request #206 from Beluga-lang/main

41daec1

merge

update syntax for propositional equality (#205)

a7fe369

* update syntax for propositional equality * empty * do not extract * don't build dune * do not run test * update comments

add rules for prop equality (#207)

5fecefe

* add rules for prop equality * bring back more files * bad naming * not enough premises

fix context subtyping (#208)

e303379

Merge branch 'main' into pr-merge-main

80c5477

Merge pull request #214 from Beluga-lang/pr-merge-main

de0694f

Port updates from the main branch

Merge pull request #216 from Beluga-lang/main

0303e99

Port Fix weird TOC (#215)

Merge remote-tracking branch 'Beluga-lang/main' into pr-fix-prop-eq-g…

12261d3

…rammar

Fix precendences to avoid weird substitution

9199213

Merge pull request #221 from Beluga-lang/pr-fix-prop-eq-grammar

b590d32

Merge main for grammar fix

Merge remote-tracking branch 'Beluga-lang/main' into pr-update-prop-e…

8b37077

…q-presup

Merge pull request #231 from Beluga-lang/pr-update-prop-eq-presup

522b9c6

Update prop eq presup

Merge branch 'main' into ext/prop-eq

604391b

Merge pull request #235 from Beluga-lang/main

cb61d68

Update CI to have (temporary) extension page

Merge remote-tracking branch 'Beluga-lang/main' into pr-port-consistency

bd5d609

Merge pull request #237 from Beluga-lang/pr-port-consistency

23772fc

Port consistency

Merge pull request #240 from Beluga-lang/main

8a8ceb2

Port notation

Optimize presup

6757806

Merge pull request #241 from Beluga-lang/pr-optimize-presup

44c8633

Optimize presup a bit

back merge (#244)

2e9760e

* Update ci_build.yaml (#242) * Simplify installation steps (#243)

Optimize a bit more

20415bb

Merge pull request #245 from Beluga-lang/pr-optimize-presup

ae037ab

Optimize a bit more

Merge remote-tracking branch 'Beluga-lang/main' into pr-port-main

a41fce1

Merge pull request #249 from Beluga-lang/pr-port-main

f689b92

Port main

Merge pull request #255 from Beluga-lang/main

0f98b91

backward merge

Add semantics for prop eq (#254)

4072e80

* Restore Semantics * Add Completeness placeholders * Add missing file * Reflect comments

Eq completeness cases and some optimization (#256)

871ae8c

* Completeness is complex * Something is wrong with PER model * Something * Some progress on completeness * Finish easy cases

Working on soundness proof (#259)

97c560d

* need to define mutual versions of lemmas * fill in the lemma * more proofs * one more case * proved a lemma * update lemmas * one more lemma * typos

Merge branch 'main' into feature/merge-from-main

295ba57

Optimize prop eq soundness a bit

553bc6a

jiangsy added 3 commits June 21, 2025 00:46

use better names

e5bf3f2

remove unnecessary handle_per_univ_elem_irrel

0b50f09

more unnecessary tactics

be1cdce

Ailrun mentioned this pull request Jun 26, 2025

introduction of Eqdep.Eq_rect_eq.eq_rect_eq (UIP) by the usage of dependent destruction #282

Closed

Ailrun added 4 commits June 26, 2025 03:33

Merge branch 'main' into port-pr-288

3ef0bf0

Merge pull request #289 from Beluga-lang/port-pr-288

1b440a9

Port #288 to ext/prop-eq

Replace conv rules with conv' helpers

dac3461

Improve tactics a bit

6ad0a86

Merge branch 'main' into ext/prop-eq

2b77d11

Merge branch 'main' into ext/prop-eq

274a659

fix rel_exp_eqrec_cong

4a7458b

Ailrun commented Jul 1, 2025

View reviewed changes

theories/Core/Completeness/LogicalRelation/Lemmas.v Outdated Show resolved Hide resolved

Ailrun and others added 6 commits July 1, 2025 13:12

Remove all UIP usages

0751c2e

Remove unused tactic

b7daa1a

Merge branch 'main' into ext/prop-eq

422057a

Merge branch 'main' into ext/prop-eq

e277824

mark todo

026381a

Merge branch 'main' into ext/prop-eq

4b79c50

Ailrun merged commit 4870ecf into main Jul 7, 2025
4 checks passed

Ailrun deleted the ext/prop-eq branch July 7, 2025 18:41

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Merge the prop equality extension #287

Merge the prop equality extension #287

Uh oh!

Ailrun commented Jun 19, 2025 •

edited

Loading

Uh oh!

Ailrun commented Jun 20, 2025

Uh oh!

jiangsy commented Jun 27, 2025

Uh oh!

Ailrun commented Jun 30, 2025

Uh oh!

jiangsy commented Jun 30, 2025

Uh oh!

jiangsy commented Jun 30, 2025 •

edited

Loading

Uh oh!

Ailrun commented Jun 30, 2025

Uh oh!

jiangsy commented Jun 30, 2025 •

edited

Loading

Uh oh!

Uh oh!

HuStmpHrrr commented Jul 7, 2025

Uh oh!

Ailrun commented Jul 7, 2025

Uh oh!

Uh oh!

Uh oh!

Merge the prop equality extension #287

Merge the prop equality extension #287

Uh oh!

Conversation

Ailrun commented Jun 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Ailrun commented Jun 20, 2025

Uh oh!

jiangsy commented Jun 27, 2025

Uh oh!

Ailrun commented Jun 30, 2025

Uh oh!

jiangsy commented Jun 30, 2025

Uh oh!

jiangsy commented Jun 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Ailrun commented Jun 30, 2025

Uh oh!

jiangsy commented Jun 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

HuStmpHrrr commented Jul 7, 2025

Uh oh!

Ailrun commented Jul 7, 2025

Uh oh!

Uh oh!

Uh oh!

Ailrun commented Jun 19, 2025 •

edited

Loading

jiangsy commented Jun 30, 2025 •

edited

Loading

jiangsy commented Jun 30, 2025 •

edited

Loading