Skip to content
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

Jump to bottom

GREEDY-GREEDY HYBRID: Refute 1516->255 #1054

Draft
wants to merge 124 commits into
base: main
Choose a base branch
from
Draft

GREEDY-GREEDY HYBRID: Refute 1516->255 #1054

wants to merge 124 commits into from
+1,006 −62

Conversation

pitmonticone
Copy link
Collaborator

@pitmonticone pitmonticone commented Jan 20, 2025 •
edited by github-actions bot
Loading

  • Complete proof of GreedyB.exists_extension
  • Fill sorrys about partial_domain and partial_range
  • Define GreedyB.Extension.next
  • Update blueprint

Co-authors: @LorenzoLuccioli, @marcop5

Closes #820

pitmonticone and others added 30 commits December 17, 2024 00:52
@pitmonticone
Update Equation1516.lean
6d23981
@LorenzoLuccioli
Add partial skeleton of the proof
27b331a 
This is a big and unpolished commit, sorry.
@LorenzoLuccioli
add partial domain and image with lemmas
00f8a7e
@LorenzoLuccioli
fix name of a lemma
aa55c55
@LorenzoLuccioli
define w and add some lemmas
2291648
@LorenzoLuccioli
add comment
f598784
@LorenzoLuccioli
add inj to OK and make arguments of aux2 implicit
414096d
@LorenzoLuccioli
update definition of w
31a7124
@LorenzoLuccioli
add definition of next with some lemmas
e7075ea
@LorenzoLuccioli
finish proof of exists_extension
b61b8a6
@LorenzoLuccioli
format
d839c12
@LorenzoLuccioli
attempt starting GreedyB
c10347a
@marcop5
add the --doable proof
2f7430e
@marcop5
Merge branch '1516-255' of https://github.com/pitmonticone/Equational…
8a1edcf 
…Theories into 1516-255
@LorenzoLuccioli
cleanup
a788829
@LorenzoLuccioli
cleanup
908831f
@LorenzoLuccioli
move x0
928cf39
@LorenzoLuccioli
small refactor of OK
8f6e838
@LorenzoLuccioli
modify exists_extension statement
6f0a584
@LorenzoLuccioli
prove op_x₀_self
eeaaa6d
@LorenzoLuccioli
add comment
fbb6e63
@LorenzoLuccioli
change definition of OK in GreedyB
43efbf0
@LorenzoLuccioli
cleanup and add some Mathlib lemmas
8d7c674
@LorenzoLuccioli
cleanup
65b6647
@LorenzoLuccioli
partial proof of exist_extension and change statement
d4ea6da
@LorenzoLuccioli
add seed and Lemmas
12a2351
@LorenzoLuccioli
cleanup
3daba84
@LorenzoLuccioli
add a check
60593e3
@pitmonticone
Merge branch 'main' into 1516-255
9c1ca40
@LorenzoLuccioli @pitmonticone
modify definition of OK
beef72a 
Co-authored-by: Pietro Monticone <[email protected]>
@LorenzoLuccioli
small cleanup
7b7d58b
@LorenzoLuccioli
add base1' and base2' without proof
848b2e1
@LorenzoLuccioli
rename exists_extension_aux in exists_useful_c and update it
1788122
@LorenzoLuccioli
rename c to useful_c
64d008c
@LorenzoLuccioli
new version of exists_extension
3f02450
@LorenzoLuccioli
new version of PartialSolution
8ed1c0b
@LorenzoLuccioli
tweak definition of OK
5a38c19
@LorenzoLuccioli
add Extension 1 and 2
a851a70
@LorenzoLuccioli
add section Extension1 with lemmas
1409d3c
@LorenzoLuccioli
add base1''
ba56ae9
@LorenzoLuccioli
fix some bugs
79a43c9
@LorenzoLuccioli
complete next1
d9e6f30
@LorenzoLuccioli
add def_trichotomy
02cab1b
@LorenzoLuccioli
add extension2
fa8e3bb
@LorenzoLuccioli
cleanup
16e32e4
@LorenzoLuccioli
small ontation change
6f670c0
@LorenzoLuccioli
fix bugs
29eaa14
@LorenzoLuccioli
finish exists_extension
85797e1
@LorenzoLuccioli
comment out old implementation
0942c53
@LorenzoLuccioli
remove unused hypothesis in exists_extra_set1
7bb426c
@LorenzoLuccioli
complete new implementation of seed
03341f7
@LorenzoLuccioli
prove last 3 sorries
a6dbfad
@LorenzoLuccioli
cleanup
67befe2
@LorenzoLuccioli
prove new version of base1
8a44c02
@LorenzoLuccioli
golf
fb59b04
@LorenzoLuccioli
clenup
e2d7ee7
@LorenzoLuccioli
prove new version of base2
a57251e
@LorenzoLuccioli
cleanup
be09354
@LorenzoLuccioli
uncomment equational_result tag
85c81a4
@LorenzoLuccioli
golf
354d2bf
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

GREEDY-GREEDY HYBRID: Refute 1516->255
3 participants
@pitmonticone @LorenzoLuccioli @marcop5