Repository navigation

Using the `rocq-coinduction` library - #285

Open

rogerburtonpatel wants to merge 195 commits into

DeepSpec:masterfrom

rogerburtonpatel:new-coinduction

Open

Using the `rocq-coinduction` library#285
rogerburtonpatel wants to merge 195 commits into
DeepSpec:masterfrom
rogerburtonpatel:new-coinduction

Commits on Jan 22, 2026
- wip: Use coinduction
  Lysxia
  committed
  9f3984c
Commits on Feb 9, 2026
- updated Eq filename in DEV.md
  rogerburtonpatel
  committed
  fc018e6
- added TODOs to Basics.v
  rogerburtonpatel
  committed
  244192b
- fixed a typo in CategoryOps
  rogerburtonpatel
  committed
  500fbbc
Commits on Feb 10, 2026
- updates to eqit
  rogerburtonpatel
  committed
  01b2a10
- some more, switching to look at hinduction
  rogerburtonpatel
  committed
  5151403
- progress. transitivity proof ongoing.
  rogerburtonpatel
  committed
  503fe44
- a bit more.
  rogerburtonpatel
  committed
  e0e55d4
Commits on Feb 12, 2026
- switching
  rogerburtonpatel
  committed
  2eb0dc9
Commits on Feb 13, 2026
- weaker eqitF_eqit proof, switching for paco comparison and high-level survey
  rogerburtonpatel
  committed
  d023014
- figured out gfp_fp, now building rich tactic library
  rogerburtonpatel
  committed
  744bada
- Created Utils.v.
  rogerburtonpatel
  committed
  2fa0ffa
- Put hinduction in Utils.v. Utils.v now in build path.
  rogerburtonpatel
  committed
  6c6e02e
- From Coq -> From Stdlib
  rogerburtonpatel
  committed
  1349eff
- Removed Core Utils.v, moved defs to Basics Utils.v
  rogerburtonpatel
  committed
  dd3d418
- Eqit.v documentation (1)
  rogerburtonpatel
  committed
  226b47d
- Eqit documentation (2)
  rogerburtonpatel
  committed
  0db57fa
- Proper proofs in Eqit.v
  rogerburtonpatel
  committed
  ff65489
- Fixed build
  rogerburtonpatel
  committed
  5762fc4
- cleaned proper proof
  rogerburtonpatel
  committed
  6b47f09
Commits on Feb 14, 2026
- Eqit.v documentation 3
  rogerburtonpatel
  committed
  6938234
- Remove paco: transitive closure of eqit
  rogerburtonpatel
  committed
  ab592c8
- Symmetry proof
  rogerburtonpatel
  committed
  cc93ebb
- Clean document
  rogerburtonpatel
  committed
  7bc2eb3
- more proof, done with eqit_gen
  rogerburtonpatel
  committed
  a0895da
Commits on Feb 17, 2026
- Moving on
  rogerburtonpatel
  committed
  ddb4459
- more: switching to master
  rogerburtonpatel
  committed
  c3b7bb1
- done up to eqit_inv.
  rogerburtonpatel
  committed
  9715c82
- strengthened Utils.v
  rogerburtonpatel
  committed
  a129e10
- tactic: strengthened simpobs
  rogerburtonpatel
  committed
  748b0f8
- done through eqit_inv
  rogerburtonpatel
  committed
  4332dc3
- transitivity-1
  rogerburtonpatel
  committed
  8392287
- Eutt is an equivalence relation.
  rogerburtonpatel
  committed
  370300c
- Strengthened and used definition of down.
  rogerburtonpatel
  committed
  798b869
- Documentation: some notes on eutt transitivity
  rogerburtonpatel
  committed
  1069773
Commits on Feb 18, 2026
- build
  rogerburtonpatel
  committed
  813d9e0
Commits on Feb 19, 2026
- done up to bind/before
  rogerburtonpatel
  committed
  db7f284
- done with hard proof: eqitgen_cong_eqit
  rogerburtonpatel
  committed
  b8a1ece
- stopping to warm up in setoid hell
  rogerburtonpatel
  committed
  1b15c1d
- done up to 3 admitted proofs
  rogerburtonpatel
  committed
  a35f0ea
- some more ideas, still cooking on it
  rogerburtonpatel
  committed
  52f71f4
Commits on Feb 20, 2026
- done w tricky bind_r proof
  rogerburtonpatel
  committed
  64460ba
- ONTO THE LAST.
  rogerburtonpatel
  committed
  8118713
Commits on Feb 21, 2026
- done with Eqit proofs. considering changing eqit_bind_clo to a parametric morphism.
  rogerburtonpatel
  committed
  5a95e68
- Fixed a few tactics
  rogerburtonpatel
  committed
  bd926b2
- Strengthened backstep, moved tactics
  rogerburtonpatel
  committed
  800aa97
- Should probably gitignore this file
  rogerburtonpatel
  committed
  1c4c190
- a comment
  rogerburtonpatel
  committed
  9df05ac
- Documentation.
  rogerburtonpatel
  committed
  c52fd16
Commits on Feb 23, 2026
- Paco removed from Eqit
  rogerburtonpatel
  committed
  2fbe700
- Documented top of Eqit.v. Refactoring paco tactics.
  rogerburtonpatel
  committed
  4b88c07
- Cleaned up proofs and documentation up to end hide
  rogerburtonpatel
  committed
  23ea5bb
- More cleaning. Reaching a fixed point of cleaning.
  rogerburtonpatel
  committed
  3a04249
- Removed some seemingly unecessary Instances, might roll back
  rogerburtonpatel
  committed
  d35379c
- Reverting
  rogerburtonpatel
  committed
  77d642b
- Added one aborted proof; removed unnecessary lines.
  rogerburtonpatel
  committed
  2744a76
- Added notes on next steps for Eqit.v
  rogerburtonpatel
  committed
  90baa05
- Pushing transitivity of eqitF true false to look at
  rogerburtonpatel
  committed
  858d476
- removed dependent induction. Pushing elem trans stuck proof.
  rogerburtonpatel
  committed
  c8c46f1
Commits on Feb 24, 2026
- notes
  rogerburtonpatel
  committed
  297497a
- Various updates w notes
  rogerburtonpatel
  committed
  39ead3a
- Done with easy equiv proof, next is eutt props
  rogerburtonpatel
  committed
  282bcba
Commits on Feb 25, 2026
- A proof of eutt's respectfulness of bind.
  rogerburtonpatel
  committed
  6b3218d
- Pushing failing proofs for sharing
  rogerburtonpatel
  committed
  b969d9b
Commits on Feb 26, 2026
- Midway through the monster.
  rogerburtonpatel
  committed
  664e894
- Progress. The horrors persist
  rogerburtonpatel
  committed
  ebdc267
Commits on Feb 27, 2026
- Done up to tau case. trying automation.
  rogerburtonpatel
  committed
  28a44fd
- Progress. 5 shelved goals.
  rogerburtonpatel
  committed
  ff8e9b2
Commits on Mar 4, 2026
- some wip on design and proofs
  YaZko
  committed
  d7e643c
Commits on Mar 5, 2026
- a few comments
  YaZko
  committed
  2208bcd
Commits on Mar 6, 2026
- Notes for meeting
  rogerburtonpatel
  committed
  dfea90b
- Missing rewriting lemma
  YaZko
  committed
  3a5567a
- Merge branch 'yannick-coinduction' of github.com:rogerburtonpatel/InteractionTrees into yannick-coinduction
  YaZko
  committed
  66fc42d
- notes on next steps
  rogerburtonpatel
  committed
  8e3862c
- fixed git things, merging into roger-coinduction next
  rogerburtonpatel
  committed
  e1e5fcc
- added new notation for eutt with R, euttge with R
  rogerburtonpatel
  committed
  902e071
- Fixing file, continuing
  rogerburtonpatel
  committed
  169b089
Commits on Mar 9, 2026
- elem proper proof, other fixes
  rogerburtonpatel
  committed
  a9763b0
- elem bind proper proof, other fixes
  rogerburtonpatel
  committed
  319b523
- Pushed bind for yannick
  rogerburtonpatel
  committed
  f5b70c3
- Merge branch 'yannick-coinduction' of github.com:rogerburtonpatel/InteractionTrees into yannick-coinduction
  rogerburtonpatel
  committed
  b76fd22
- Removed some git garbage
  rogerburtonpatel
  committed
  923f8ec
Commits on Mar 10, 2026
- Some new proofs, improvements to subrelation proofs
  rogerburtonpatel
  committed
  e4f102e
- Some proof speedups. next is more proper proofs
  rogerburtonpatel
  committed
  f1ca7e7
- Using some notation more
  rogerburtonpatel
  committed
  3204097
Commits on Mar 16, 2026
Commits on Mar 17, 2026
- Few small changes from meeting
  rogerburtonpatel
  committed
  2936309
- UpToTaus working after <20mins work
  rogerburtonpatel
  committed
  61b7b2e
Commits on Mar 19, 2026
- Updated comments, now fixing step and unstep
  rogerburtonpatel
  committed
  5dd6f48
- Progress, but trickiness with bind and coinduction.
  rogerburtonpatel
  committed
  ab6fdc7
- ideas for new closures
  rogerburtonpatel
  committed
  3001b71
Commits on Mar 23, 2026
- Eqit builds, pushing with a note
  rogerburtonpatel
  committed
  80863cb
- Small cleanup, trying generalized gfp
  rogerburtonpatel
  committed
  f55eb91
- forall X Y : type under the gfp
  rogerburtonpatel
  committed
  6059d48
Commits on Mar 26, 2026
- Done through KTreeFacts
  rogerburtonpatel
  committed
  c946fd3
- Done through TranslateFacts
  rogerburtonpatel
  committed
  eb83f55
- Done up to more. Horror.
  rogerburtonpatel
  committed
  25446ac
Commits on Mar 27, 2026
- Done through InterpFacts
  rogerburtonpatel
  committed
  74e8635
- Grind.
  rogerburtonpatel
  committed
  a5d0fa8
- Consoloated EuttExtras; done w SimUpToTaus
  rogerburtonpatel
  committed
  4a4d48f
Commits on Mar 30, 2026
- Done up through HandlerFacts, now on Rutt
  rogerburtonpatel
  committed
  2c155fe
- Removed UpToTaus.v
  rogerburtonpatel
  committed
  2e14238
- Removed UpToTaus dependencies
  rogerburtonpatel
  committed
  3daa15e
- Changes to Rutt, IP
  rogerburtonpatel
  committed
  498e403
- Done with Rutt.
  rogerburtonpatel
  committed
  247e515
- Reintroduce eret, etau, evis tactics.
  rogerburtonpatel
  committed
  7242662
- StateFacts.v
  rogerburtonpatel
  committed
  d23471c
- Working on eutt_conj detail for has_post
  rogerburtonpatel
  committed
  8818a31
Commits on Mar 31, 2026
- build, switching for demo
  rogerburtonpatel
  committed
  b7accc7
- Refactor subrelationH, done w HasPost
  rogerburtonpatel
  committed
  c90131f
- In Leaf.v, now considering eqit_Leaf_bind_clo. Also pivoting to rewrite strategies.
  rogerburtonpatel
  committed
  cf68c57
Commits on Apr 1, 2026
- Refactor names
  rogerburtonpatel
  committed
  37c1828
Commits on Apr 8, 2026
Commits on Apr 10, 2026
- Progress, though slow. Continuing.
  rogerburtonpatel
  committed
  4d6b954
Commits on Apr 13, 2026
- Done with RuttFacts, moving on
  rogerburtonpatel
  committed
  e35d4d3
- Added TODOs
  rogerburtonpatel
  committed
  e8ac446
- Done through Finite.v
  rogerburtonpatel
  committed
  840dc66
Commits on Apr 14, 2026
- Progress, switching for meeting
  rogerburtonpatel
  committed
  ff373c9
Commits on Apr 15, 2026
- Done up to iForest. That next.
  rogerburtonpatel
  committed
  96959d2
Commits on Apr 20, 2026
- Some more care with iForest.v.
  rogerburtonpatel
  committed
  0a7240a
Commits on Apr 21, 2026
- removed a print stmt
  rogerburtonpatel
  committed
  9b3182d
- iForest progress, better tactics. Long road of a file.
  rogerburtonpatel
  committed
  a806a29
Commits on Apr 23, 2026
- Done with IForest.
  rogerburtonpatel
  committed
  210b6f2
- Some refactoring. Done up to deterimize in itracefacts.
  rogerburtonpatel
  committed
  dc79d5d
- Done with more extras, saving for now.
  rogerburtonpatel
  committed
  d77d847
- More progress.
  rogerburtonpatel
  committed
  8a76373
Commits on Apr 27, 2026
- Done with IterRel
  rogerburtonpatel
  committed
  63dab15
- Done with DelaySpecMonad
  rogerburtonpatel
  committed
  f3f314b
- Done with StateSpecT
  rogerburtonpatel
  committed
  408c19c
Commits on Apr 30, 2026
- Done with ITraceFacts.
  rogerburtonpatel
  committed
  43ad6f4
Commits on May 1, 2026
- Some small Dijkstra work
  rogerburtonpatel
  committed
  79c8d87
- Add makefile.d to gitignore
  rogerburtonpatel
  committed
  ca69fca
- Merge branch 'new-gfp' of github.com:rogerburtonpatel/InteractionTrees into new-gfp
  rogerburtonpatel
  committed
  b1ecba3
- Various small tweaks. Now onto rutt gfp forall refactor.
  rogerburtonpatel
  committed
  2f500d4
- Notes and ideas on stepping
  rogerburtonpatel
  committed
  aa50164
Commits on May 3, 2026
- Changed CIH, much progress on ITreeDijkstra.
  rogerburtonpatel
  committed
  03311e3
Commits on May 4, 2026
- Sweeping progress on extras. Committing to check master.
  rogerburtonpatel
  committed
  e9d2e9e
- Progress on itracebind.
  rogerburtonpatel
  committed
  abb2d37
- hey this sux
  rogerburtonpatel
  committed
  de8029c
- Improved HandlerFacts build time by 32x, Translate by unmeasured amt
  rogerburtonpatel
  committed
  319670a
- Cleaned scripts.
  rogerburtonpatel
  committed
  254bc8e
- Various other progress on extras.
  rogerburtonpatel
  committed
  4c5c813
- Removed Paco2.v.
  rogerburtonpatel
  committed
  a0b4c7a
- Builds. No longer tracking .Makefile.d.
  rogerburtonpatel
  committed
  d8ecfa5
- Start of many timing experiments. Developing vsrocq extension.
  rogerburtonpatel
  committed
  a9b341d
Commits on May 5, 2026
- Makefile.conf to .gitignore
  rogerburtonpatel
  committed
  bdff9f0
- Timings on M1, speedups in exceptionsfacts.v
  rogerburtonpatel
  committed
  c7c8413
- Progress on ITraceFacts.
  rogerburtonpatel
  committed
  d078f58
- Done with ITraceBind.
  rogerburtonpatel
  committed
  af42b0d
Commits on May 11, 2026
- Much progress. Onto PureITreeDijkstra.v.
  rogerburtonpatel
  committed
  a810141
- More timing. Switching to examine PureITD.
  rogerburtonpatel
  committed
  98dd5fd
- Done with PureITreeDijkstra.v
  rogerburtonpatel
  committed
  541ae19
- Done with TracesIT.v
  rogerburtonpatel
  committed
  e983f5e
- Done with StateIOTrace.v
  rogerburtonpatel
  committed
  f36a2ca
- Done up to part of SecureEqEuttHalt.
  rogerburtonpatel
  committed
  5b4ad41
- Done with SecureEqEuttHalt, needs speedups.
  rogerburtonpatel
  committed
  96772f4
Commits on May 12, 2026
Commits on May 13, 2026
- Progress and new lemmas. switching for check
  rogerburtonpatel
  committed
  d914e89
- Done, continuing
  rogerburtonpatel
  committed
  0b32b6c
Commits on May 15, 2026
- Done with SecureEqWcompat
  rogerburtonpatel
  committed
  dad885f
Commits on May 18, 2026
- Progress. Nearly done.
  rogerburtonpatel
  committed
  88777c3
Commits on May 19, 2026
- Fixed ITraceBind Admitted
  rogerburtonpatel
  committed
  64852e0
- Timing and so forth
  rogerburtonpatel
  committed
  ea0d564
Commits on May 20, 2026
- Final couple of files
  rogerburtonpatel
  committed
  6b6f523
Commits on May 22, 2026
- Done up to ProgInsens and after, fixing a bug
  rogerburtonpatel
  committed
  48589de
- DONE
  rogerburtonpatel
  committed
  c83d2a9
- Builds. Examples fixing.
  rogerburtonpatel
  committed
  782e7c1
Commits on May 23, 2026
- It's done.
  rogerburtonpatel
  committed
  6981e41
Commits on May 26, 2026
- Done with Imp Examples.
  rogerburtonpatel
  committed
  9f8631c
Commits on May 28, 2026
- Some adjustments after demo
  rogerburtonpatel
  committed
  8dff6d7
Commits on May 29, 2026
- Changed eqit arg order back to original to improve backwards compatibility
  rogerburtonpatel
  committed
  4fe9aaf
Commits on Jun 1, 2026
- More powerful tower induction automation for inf_closed
  rogerburtonpatel
  committed
  c018993
Commits on Jun 3, 2026
- Change to use first iteration of mon_auto
  rogerburtonpatel
  committed
  4ddc378
- Strong monauto
  rogerburtonpatel
  committed
  649b40d
Commits on Jun 4, 2026
- Removed a comment
  rogerburtonpatel
  committed
  fdf1096
Commits on Jun 8, 2026
- Improved chain tactics
  rogerburtonpatel
  committed
  bee6647
- Rm Monauto error message, for later
  rogerburtonpatel
  committed
  3d161cb
Commits on Jun 9, 2026
- Slight improvement to monauto
  rogerburtonpatel
  committed
  5e7580f
Commits on Jun 23, 2026
- removed some comments
  rogerburtonpatel
  committed
  62b8b51
Commits on Jun 29, 2026
- Final rewrites modulo paco in examples.
  rogerburtonpatel
  committed
  40b99ca
- Removed timing experiments before PR
  rogerburtonpatel
  committed
  beaa25c
- Merge branch 'master' into new-coinduction
  rogerburtonpatel
  authored
  f0d99e0
- Remove garbage files 1
  rogerburtonpatel
  authored
  3631b51
Commits on Jun 30, 2026
- change paco dep to rocq-coinduction
  rudynicolop
  committed
  116385d
- restore Makefile and _CoqProject
  rudynicolop
  committed
  1e41738
- Merge pull request #1 from rudynicolop/rudy/pr/285
  rogerburtonpatel
  authored
  565ab2a
- paco -> rocq coinduction
  rogerburtonpatel
  committed
  a945a2d
- Removed more dead files
  rogerburtonpatel
  committed
  dea3201
Commits on Jul 25, 2026
- Simplify a proof, write TODOs
  rogerburtonpatel
  committed
  d34881b

Commits

Commits on Jan 22, 2026

Commits on Feb 9, 2026

Commits on Feb 10, 2026

Commits on Feb 12, 2026

Commits on Feb 13, 2026

Commits on Feb 14, 2026

Commits on Feb 17, 2026

Commits on Feb 18, 2026

Commits on Feb 19, 2026

Commits on Feb 20, 2026

Commits on Feb 21, 2026

Commits on Feb 23, 2026

Commits on Feb 24, 2026

Commits on Feb 25, 2026

Commits on Feb 26, 2026

Commits on Feb 27, 2026

Commits on Mar 4, 2026

Commits on Mar 5, 2026

Commits on Mar 6, 2026

Commits on Mar 9, 2026

Commits on Mar 10, 2026

Commits on Mar 16, 2026

Commits on Mar 17, 2026

Commits on Mar 19, 2026

Commits on Mar 23, 2026

Commits on Mar 26, 2026

Commits on Mar 27, 2026

Commits on Mar 30, 2026

Commits on Mar 31, 2026

Commits on Apr 1, 2026

Commits on Apr 8, 2026