Skip to content

Jacob/itree separation logic #1180

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jeprinz wants to merge 76 commits into
base: main
Choose a base branch
from
Open

Jacob/itree separation logic #1180

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
76 commits
Select commit Hold shift + click to select a range
11fa6d1
some progress on generalizing spec, dspec
jeprinz May 26, 2026
56213dc
some progress on generalizing spec_mono and spec_bind
jeprinz May 26, 2026
d3389b3
generalized discr tree lookup to different spec thms
jeprinz May 26, 2026
ec869b9
use discr tree, dspec partially working
jeprinz May 27, 2026
442c2a7
dspec working, need lifting
jeprinz May 27, 2026
1f4cca0
lifting works
jeprinz May 28, 2026
eadd310
command for registering spec statements
jeprinz May 28, 2026
7450fd5
wip partial fixpoint induction tactic
jeprinz Jun 1, 2026
7169830
got all the parts working individually
jeprinz Jun 2, 2026
59d1de4
cleaned up UnfoldPF.lean
jeprinz Jun 2, 2026
12a67e3
cleaned up more
jeprinz Jun 2, 2026
bc15c24
fixed bug, and found another issue
jeprinz Jun 3, 2026
a429a66
checkpoint, still issues with pf variations
jeprinz Jun 3, 2026
42f4bb0
fixed the bugs
jeprinz Jun 3, 2026
462ae09
tutorial and cleaned up code
jeprinz Jun 3, 2026
f19b19c
Merge branch 'jacob/spec-extensions-dspec' of https://github.com/Aene…
jeprinz Jun 3, 2026
fa8c069
fixed some merge issues
jeprinz Jun 3, 2026
d447531
reordered tactics to preserve old behavior
jeprinz Jun 12, 2026
649686d
used get? instead of get!
jeprinz Jun 12, 2026
96fb2bf
tests update
jeprinz Jun 15, 2026
84fb945
error test
jeprinz Jun 15, 2026
8db6588
update tests, fix tutorial
jeprinz Jun 15, 2026
533dfac
Update tests/lean/Tutorial/Solutions.lean
jeprinz Jun 17, 2026
5b2d606
Apply suggestions from code review
jeprinz Jun 19, 2026
0822cfc
examples with first/second_arg_const
jeprinz Jun 19, 2026
870c028
reservedNameAction
jeprinz Jun 19, 2026
04e82fb
changed div syntax and added delaborator
jeprinz Jun 19, 2026
e384caf
fixed formatting, renamed file, improved tutorial
jeprinz Jun 19, 2026
3bf1346
Merge remote-tracking branch 'origin/main' into spec-extensions-dspec
jeprinz Jun 19, 2026
8d8f6c7
generalized spec_to_mvcgen
jeprinz Jun 19, 2026
0ebb58f
copied in coinductive library and itrees
jeprinz Jun 19, 2026
3f02768
start working on hoare logic spec statement
jeprinz Jun 19, 2026
77f1f85
Use trait to make opaque hash function
jeprinz Jun 19, 2026
eec2706
Merge remote-tracking branch 'origin/main' into spec-extensions-dspec
jeprinz Jun 22, 2026
40f5109
Merge remote-tracking branch 'origin/spec-extensions-dspec' into jaco…
jeprinz Jun 22, 2026
f4d51b8
Apply suggestions from code review
jeprinz Jun 23, 2026
30aee16
more work on spec for itree
jeprinz Jun 23, 2026
801ac5c
some small fixes from code review
jeprinz Jun 23, 2026
8ed3490
generalized getPostNamesFromGoal and renamed spec_name
jeprinz Jun 23, 2026
b496f29
Merge remote-tracking branch 'origin/main' into spec-extensions-dspec
jeprinz Jun 23, 2026
f6162aa
fixed state extension bug
jeprinz Jun 23, 2026
a29e8d3
Merge remote-tracking branch 'origin/spec-extensions-dspec' into jaco…
jeprinz Jun 23, 2026
86a2443
progress on ITree based spec example
jeprinz Jun 23, 2026
8458994
lifting feature in Step, lift works now with coinSpec
jeprinz Jun 24, 2026
292974e
plan for result being itree
jeprinz Jun 24, 2026
9914155
lifting for assumptions and `step with` + tests
jeprinz Jun 24, 2026
4ad2754
Merge branch 'spec-extensions-dspec' into jacob/itree-separation-logic
jeprinz Jun 24, 2026
27345a9
some more itree tests
jeprinz Jul 1, 2026
ec3b030
some progress converting Result to ITree, errors
jeprinz Jul 2, 2026
2e948ba
some progress on various fronts
jeprinz Jul 3, 2026
24d67e8
some more progress on ITree eliminators
jeprinz Jul 6, 2026
1e58546
theorems for computing ITree dependent eliminator
jeprinz Jul 7, 2026
b27cee5
will give eliminator one case per effect
jeprinz Jul 7, 2026
2564078
fixed many of the Result match issues
jeprinz Jul 7, 2026
e28578f
more progress to fixing ITree migration
jeprinz Jul 7, 2026
ffc411b
more progress fixing migration errors
jeprinz Jul 8, 2026
95d535f
a bunch more work on updating to new Result
jeprinz Jul 10, 2026
70b8b4d
Merge remote-tracking branch 'origin/main' into jacob/itree-separatio…
jeprinz Jul 10, 2026
67414da
fixed do-elab bug caused by Result reducibility
jeprinz Jul 13, 2026
3162d32
fixed dspec admissibility with ITree
jeprinz Jul 14, 2026
ded4e4f
fixed all errors in backend
jeprinz Jul 14, 2026
1546bd9
assert issue
jeprinz Jul 15, 2026
26c5f65
some progress to fixing assertions
jeprinz Jul 16, 2026
2be6bae
fixed assert issue
jeprinz Jul 16, 2026
f7c00b0
fixed all errors from ITree migration
jeprinz Jul 17, 2026
c1a707b
cleaned up some definitions
jeprinz Jul 17, 2026
6593d65
improved Result matching, easier to add effects
jeprinz Jul 20, 2026
72f9852
fixed matches in tests
jeprinz Jul 20, 2026
fc93b20
proofs work with any effects (hopefully)
jeprinz Jul 20, 2026
64cbe62
delete test effect
jeprinz Jul 20, 2026
dccdea0
Merge remote-tracking branch 'origin/main' into jacob/itree-separatio…
jeprinz Jul 20, 2026
e5f73a9
clean up comments and old code
jeprinz Jul 22, 2026
0b753e2
reinstated mvcgen
jeprinz Jul 22, 2026
b3ddc6c
Made mvcgen work with further effects
jeprinz Jul 22, 2026
13f7340
Cleaned up more comments
jeprinz Jul 22, 2026
4ec5b5b
Slice.clone, List.clone, Slice.fill may use effs
jeprinz Jul 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion backends/lean/Aeneas/Command/Decompose/Tests.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1570,7 +1570,7 @@ info: test39_eq : ∀ (n : ℕ),
#guard_msgs in
#check @test39_eq
/--
info: 'Aeneas.Command.Decompose.Tests.test39_eq' depends on axioms: [propext, Quot.sound]
info: 'Aeneas.Command.Decompose.Tests.test39_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms test39_eq
Expand Down
Loading
Loading