paco => rocq-coinduction - #1514

Draft

rudynicolop wants to merge 31 commits into

jasmin-lang:mainfrom

rudynicolop:rocq-coinduction

Commits on Jul 17, 2026

rocq-coinduction: modify config files
rudynicolop
committed
e0b92e6
rocq-coinduction: began while file, ITrees may need more/better Proper instances
rudynicolop
committed
1cfb8e8
rocq-coinduction: while.v with admitted instance, began xrutt.v refactor
rudynicolop
committed
b8106f5
rocq-coinduction: it_exec.v refactor, hide trans_clo infra from xrutt.v
rudynicolop
committed
54387f5
rocq-coinduction: move section var for xruttF, progress on xrutt Proper instance proofs based on rutt proof
rudynicolop
committed
8855ce1
rocq-coinduction: refactor rec_facts.v
rudynicolop
committed
2ef2228
rocq-coinduction: began repairing xrutt_cong_eutt
rudynicolop
committed
e96c72a
rocq-coinduction: adhering to upstream xrutt_cong_eutt style more difficult
rudynicolop
committed
ab18158
rocq-coinduction: xrutt_cong_eutt style mimicing rutt_cong_eutt
rudynicolop
committed
3aa3492
rocq-coinduction: xrutt_cong_eutt EqTau and EqVis cases
rudynicolop
committed
3d0697b
rocq-coinduction: xrutt_cong_eutt refactored (TODO: maybe try to recover upstream proof strategy or update comments)
rudynicolop
committed
d077199
rocq-coinduction: xrutt_bind
rudynicolop
committed
87269a1
rocq-coinduction: xrutt interp_mrec lemma
rudynicolop
committed
6042c76
rocq-coinduction: xrutt blocked by question, it_sems_core refactored
rudynicolop
committed
d539170
ensure [xrutt] is compatible with ITree.bind reasoning in coinduction proofs
rudynicolop
committed
5069b40
rocq-coinduction: xrutt_facts proof repair
rudynicolop
committed
55d78b2
rocq-coinduction: repaired xrutt_facts proofs
rudynicolop
committed
b65678a
rocq-coinduction: failed attempt to resolve eq_itree rewriting in eqit false true goals
rudynicolop
committed
f35d995
rocq-coinduction: need rutt_mon's R1 R2 universally quantified under sim for bind rreasoning
rudynicolop
committed
a80573b
rocq-coinduction: use my rutt_mon bind laws from my fork to prove rutt_extras
rudynicolop
committed
d2af3b3
rocq-coinduction: refactored core_logics
rudynicolop
committed
7717d71
rocq-coinduction: refactored mix_to_small_steps.v
rudynicolop
committed
12e22fc
rocq-coinduction: refactored hoare and relation logic
rudynicolop
committed
d775420
rocq-coinduction: refactored psem
rudynicolop
committed
34f3767
rocq-coinduction: fix ssr apply errors, maybe I am on the wrong version or have bad dependencies?
rudynicolop
committed
f6a0cac
rocq-coinduction: it linearization proof
rudynicolop
committed
35d64b5
rocq-coinduction: finished compiler proofs, some changes may be due to spurious errors from using a difference rocq version
rudynicolop
committed
87c9c0b
rocq-coinduction: eqit_iter_n => eutt_iter_n since some forms of rewriting for arbitrary b1 b2 in eqit no longer seem supported
rudynicolop
committed
aa2f9d9
removed dead bind_clo code
rudynicolop
committed
2ed5431
authors
rudynicolop
committed
0fa8b30
rocq-coinduction: fixed rutt argument order change and dependency
rudynicolop
committed
f28da54

Navigation Menu

Uh oh!

paco => rocq-coinduction - #1514

paco => rocq-coinduction#1514
rudynicolop wants to merge 31 commits into
jasmin-lang:mainfrom
rudynicolop:rocq-coinduction

Commits on Jul 17, 2026

rocq-coinduction: modify config files

rocq-coinduction: began while file, ITrees may need more/better Proper instances

rocq-coinduction: while.v with admitted instance, began xrutt.v refactor

rocq-coinduction: it_exec.v refactor, hide trans_clo infra from xrutt.v

rocq-coinduction: move section var for xruttF, progress on xrutt Proper instance proofs based on rutt proof

rocq-coinduction: refactor rec_facts.v

rocq-coinduction: began repairing xrutt_cong_eutt

rocq-coinduction: adhering to upstream xrutt_cong_eutt style more difficult

rocq-coinduction: xrutt_cong_eutt style mimicing rutt_cong_eutt

rocq-coinduction: xrutt_cong_eutt EqTau and EqVis cases

rocq-coinduction: xrutt_cong_eutt refactored (TODO: maybe try to recover upstream proof strategy or update comments)

rocq-coinduction: xrutt_bind

rocq-coinduction: xrutt interp_mrec lemma

rocq-coinduction: xrutt blocked by question, it_sems_core refactored

ensure [xrutt] is compatible with ITree.bind reasoning in coinduction proofs

rocq-coinduction: xrutt_facts proof repair

rocq-coinduction: repaired xrutt_facts proofs

rocq-coinduction: failed attempt to resolve eq_itree rewriting in eqit false true goals

rocq-coinduction: need rutt_mon's R1 R2 universally quantified under sim for bind rreasoning

rocq-coinduction: use my rutt_mon bind laws from my fork to prove rutt_extras

rocq-coinduction: refactored core_logics

rocq-coinduction: refactored mix_to_small_steps.v

rocq-coinduction: refactored hoare and relation logic

rocq-coinduction: refactored psem

rocq-coinduction: fix ssr apply errors, maybe I am on the wrong version or have bad dependencies?

rocq-coinduction: it linearization proof

rocq-coinduction: finished compiler proofs, some changes may be due to spurious errors from using a difference rocq version

rocq-coinduction: eqit_iter_n => eutt_iter_n since some forms of rewriting for arbitrary b1 b2 in eqit no longer seem supported

removed dead bind_clo code

authors

rocq-coinduction: fixed rutt argument order change and dependency