Merged
Conversation
Member
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 66d516b. |
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 22, 2023
|
eric-wieser
reviewed
Oct 23, 2023
Comment on lines
+44
to
+48
| theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} | ||
| (h₁ : p₁ = p₂) | ||
| (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a) | ||
| : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) := by | ||
| subst h₁; simp [← h₂] |
Contributor
There was a problem hiding this comment.
This is true more generally for Sort u:
Suggested change
| theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} | |
| (h₁ : p₁ = p₂) | |
| (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a) | |
| : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) := by | |
| subst h₁; simp [← h₂] | |
| theorem forall_domain_congr {p₁ p₂ : Sort u} {q₁ : p₁ → Sort v} {q₂ : p₂ → Sort v} | |
| (h₁ : p₁ = p₂) | |
| (h₂ : ∀ a : p₂, q₁ (h₁.mpr a) = q₂ a) | |
| : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) := by | |
| subst h₁ | |
| have : q₁ = q₂ := funext h₂ | |
| subst this | |
| rfl |
eric-wieser
reviewed
Oct 23, 2023
Comment on lines
+735
to
+744
| /- Using | ||
| ``` | ||
| theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} | ||
| (h₁ : p₁ = p₂) | ||
| (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a) | ||
| : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a) | ||
| ``` | ||
| Remark: we should consider whether we want to add congruence lemma support for arbitrary `forall`-expressions. | ||
| Then, the theroem above can be marked as `@[congr]` and the following code deleted. | ||
| -/ |
Contributor
There was a problem hiding this comment.
Probably you already saw #1926 (comment), but in case you didn't; I stumbled across what might be a neat trick to enable this behavior (and probably also arrow support in calc); define
-- an alias for `∀` to thwart checks that complain that `∀` is not a function
def Forall {α} (β : α → Sort _) := ∀ a, β aand temporarily replace ∀ with Forall when looking for congruence lemmas / Trans instances, such that the existing code-path for Expr.app can be reused.
This was referenced Jan 4, 2024
This was referenced Feb 17, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.