Skip to content

[Merged by Bors] - feat: port itauto from lean 3 #9398

Closed
digama0 wants to merge 11 commits intomasterfrom
itauto
Closed

[Merged by Bors] - feat: port itauto from lean 3 #9398
digama0 wants to merge 11 commits intomasterfrom
itauto

Conversation

@digama0
Copy link
Copy Markdown
Member

@digama0 digama0 commented Jan 2, 2024

This tactic solves problems in intuitionistic propositional logic. It also produces nice proofs when doing so, so it is useful even for proving classical theorems (using the itauto! variant to enable EM) and observing the results with #explode.

example (p : Prop) : ¬(p ↔ ¬p) := by itauto

Open in Gitpod

github-actions[bot]
github-actions bot reviewed Jan 2, 2024
View reviewed changes
@digama0 digama0 force-pushed the itauto branch 2 times, most recently from 8bc4837 to a86db51 Compare January 2, 2024 08:18
@digama0 digama0 force-pushed the itauto branch 2 times, most recently from f12c65d to 63daeaa Compare May 20, 2024 19:45
@digama0 digama0 added the t-meta Tactics, attributes or user commands label May 21, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 22, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 12, 2024

PR summary efaf55714d

Import changes

No significant changes to the import graph

Declarations diff

+ AndKind
+ AndKind.cmp
+ AndKind.sides
+ Context
+ Context.format
+ Context.withAdd
+ IProp
+ IProp.and
+ IProp.cmp
+ IProp.eq
+ IProp.format
+ IProp.iff
+ IProp.not
+ IProp.xor
+ Proof
+ Proof.app
+ Proof.check
+ Proof.exfalso
+ Proof.format
+ Proof.orElim
+ freshName
+ instance : DecidableRel (@LT.lt IProp _) := fun _ _ => inferInstanceAs (Decidable (_ = _))
+ instance : Inhabited AndKind := ⟨AndKind.and⟩
+ instance : Inhabited IProp := ⟨IProp.true⟩
+ instance : Inhabited Proof := ⟨Proof.triv⟩
+ instance : LT IProp := ⟨fun p q => p.cmp q = .lt⟩
+ instance : Std.ToFormat Context := ⟨Context.format⟩
+ instance : Std.ToFormat IProp := ⟨IProp.format⟩
+ instance : Std.ToFormat Proof := ⟨Proof.format⟩
+ isOk
+ itautoCore
+ mapProof
+ prover.
+ whenOk

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@kmill
Copy link
Copy Markdown
Contributor

kmill commented Jun 12, 2024

Looks good to me

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 12, 2024

✌️ digama0 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 12, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 12, 2024
@digama0
Copy link
Copy Markdown
Member Author

digama0 commented Jun 12, 2024

bors r+

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jun 12, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 12, 2024
@digama0
feat: port itauto from lean 3 (#9398)
9035d15 
This tactic solves problems in intuitionistic propositional logic. It also produces nice proofs when doing so, so it is useful even for proving classical theorems (using the `itauto!` variant to enable EM) and observing the results with `#explode`.
```lean
example (p : Prop) : ¬(p ↔ ¬p) := by itauto
```



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 12, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: port itauto from lean 3 [Merged by Bors] - feat: port itauto from lean 3 Jun 12, 2024
@mathlib-bors mathlib-bors bot closed this Jun 12, 2024
@mathlib-bors mathlib-bors bot deleted the itauto branch June 12, 2024 18:55
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@digama0 @AntoineChambert-Loir
feat: port itauto from lean 3 (#9398)
44e0fec 
This tactic solves problems in intuitionistic propositional logic. It also produces nice proofs when doing so, so it is useful even for proving classical theorems (using the `itauto!` variant to enable EM) and observing the results with `#explode`.
```lean
example (p : Prop) : ¬(p ↔ ¬p) := by itauto
```



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@Komyyy Komyyy mentioned this pull request Jul 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@github-actions github-actions[bot] github-actions[bot] left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@digama0 @kmill