Recent Questions - Proof Assistants Stack Exchange most recent 30 from proofassistants.stackexchange.com 2022-09-26T10:27:36Z https://proofassistants.stackexchange.com/feeds https://creativecommons.org/licenses/by-sa/4.0/rdf https://proofassistants.stackexchange.com/q/1759 2 How to unfold definitions in Lean / find the right theorems to apply? Pieter Cuijpers https://proofassistants.stackexchange.com/users/1710 2022-09-23T15:37:49Z 2022-09-23T21:05:17Z <p>After a few days playing around with Lean4, I notice I keep running into the problem of how to find the right theorems to apply. The situation below is one I run into particularly often, so perhaps I simply have not found the right tactic yet.</p> <p>Note, that there is - of course - simpler proof for this particular theorem, but for the sake of the example assume I'm looking for the indicated unfolding steps.</p> <pre><code>example (x y : α × β) : x = y ↔ (x.1 = y.1 ∧ x.2 = y.2) := by constructor . intro constructor . admit -- what can I do to unfold =' into its definition here? . congr -- I found that this one helps to solve the goal, but I wanted to unfold the assumption! . intro . admit -- what can I do to unfold =' into its definition here? </code></pre> <p>I suspected there would be something of the kind <code>apply Eq</code> or some kind of <code>intro</code> based on a constructor, or some extensionality principle. But I can't find it.</p> <p>I also find it a bit difficult to explain what I'm looking for really. The manuals do not go very deeply into giving examples of how to do proofs. (Is there a good reference with examples, perhaps?)</p> https://proofassistants.stackexchange.com/q/1753 1 Question about default definitions in fields Pieter Cuijpers https://proofassistants.stackexchange.com/users/1710 2022-09-22T08:06:15Z 2022-09-22T15:34:44Z <p>In <a href="https://proofassistants.stackexchange.com/questions/1749/unclarity-about-preorder-class-in-lean4/1750#comment3839_1750">Unclarity about Preorder class in Lean4</a> I asked why the third and fourth field (lt and lt_iff_le_not_le) in the definition of MyPreorder below would both be necessary, as one follows from the other as far as I can see. The answer was that this happens because there is no clear preference over defining LE or LT - hence the fourth line - and that the third line is there for convenience, as a default definition.</p> <p>However, if I next want to build a product preorder, it seems that I do need to repeat the definition of lt, even though it was expected to be a default? At least, if I leave it out, the assumptions at the end of the proof do not get resolved properly anymore. Notably, Lean does not ask me to define lt, it just doesn't recognize that I mean the default definition aparently.</p> <pre><code>class MyPreorder.{u} (α : Type u) extends LE α, LT α := (le_refl : ∀ a : α, a ≤ a) (le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c) (lt := λ a b =&gt; a ≤ b ∧ ¬ b ≤ a) -- default definition introduced for convenience (lt_iff_le_not_le : ∀ a b : α, a &lt; b ↔ (a ≤ b ∧ ¬ b ≤ a)) -- expected relation between lt and le instance MyProd_Preorder [P : MyPreorder α] [Q : MyPreorder β] : MyPreorder (Prod α β) where le := fun x y =&gt; x.fst ≤ y.fst ∧ x.snd ≤ y.snd lt := λ a b =&gt; a ≤ b ∧ ¬ b ≤ a -- WHY DO I HAVE TO REPEAT THE DEFAULT ? le_refl := by intros constructor . apply P.le_refl . apply Q.le_refl le_trans := by intros x y z intros a b have ineq1 := And.left a have ineq2 := And.right a have ineq3 := And.left b have ineq4 := And.right b constructor . apply P.le_trans _ _ _ ineq1 ineq3 . apply Q.le_trans _ _ _ ineq2 ineq4 lt_iff_le_not_le := by intros x y constructor . intro assumption . intro assumption </code></pre> <p>I'm not entirely sure however whether this is really the problem, or it's just my inability in Lean. A related attempt to just derive lt_iff_le_not_le from the definition of lt also fails. So perhaps I'm doing something different wrong...</p> <pre><code>class AnotherPreorder.{u} (α : Type u) extends LE α, LT α := (le_refl : ∀ a : α, a ≤ a) (le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c) (lt := λ a b =&gt; a ≤ b ∧ ¬ b ≤ a) -- default definition introduced for convenience -- I've left out the iff relation from this definition, in order to try to derive it... example (α : Type u) [P : AnotherPreorder α] : ∀ a b : α, a &lt; b ↔ (a ≤ b ∧ ¬ b ≤ a) := by intros a b constructor . intro assumption -- these fail miserably, and I don't understand why, as they do work in the other example... . intro assumption -- these fail miserably, and I don't understand why, as they do work in the other example... <span class="math-container"></span> </code></pre> https://proofassistants.stackexchange.com/q/1752 6 Why are impredicative constructions used less in type theory than in material set theory? Trebor https://proofassistants.stackexchange.com/users/78 2022-09-22T01:11:10Z 2022-09-25T14:31:51Z <p>Many infinitary objects in (say) ZFC are constructed with impredicative principles. The natural numbers are formed by intersecting every inductive set (whose existence is given by the axiom of infinity). <span class="math-container">$\sigma$</span>-algebras are generated by intersecting all <span class="math-container">$\sigma$</span>-algebras containing the generators; and many algebra textbooks define the generation of subgroups/ideals/subrings etc with this method.</p> <p>However, although there are such examples in type theory, we don't use that very often even in proof assistants with built-in impredicativity. The natural numbers in Coq are still constructed with inductive types, which are considered predicative. There seems to be some difficulty using the impredicative definitions. Is it only because we don't use excluded middle, or is it some property of type theory that makes it biased towards the predicative side?</p> https://proofassistants.stackexchange.com/q/1749 5 Unclarity about Preorder class in Lean4 Pieter Cuijpers https://proofassistants.stackexchange.com/users/1710 2022-09-21T20:49:30Z 2022-09-24T12:48:44Z <p>I realize the port of Mathlib to Lean4 is not finished yet, but I've run into a definition that I do not quite understand. I'm quite new at using theoremprovers as well as stackexchange, so please be patient with me :-)</p> <p>The class Preorder is defined as follows (relying on the standard LE and LT for defining order and strict order relations):</p> <pre><code>universe u class Preorder (\alpha : Type u) extends LE \alpha, LT \alpha := (le_refl : \forall a : \alpha, a \leq a) (le_trans : \forall a b c : \alpha, a \leq b \impl b \leq c \impl a \leq c) (lt := \lambda a b =&gt; a \leq b \and \neg b \leq a) (lt_iff_le_not_le : \forall a b : \alpha, a &lt; b \iff (a \leq b \and \not b \leq a)) </code></pre> <p>My question is: <em>why are the last two lines both necessary?</em> Each of them can, as far as I can see, be considered a definition. In particular, I've managed to derive the former from the latter as follows (defining my own MyPreorder for the purpose of showing what I mean):</p> <pre><code>universe u class MyPreorder (\alpha : Type u) extends LE \alpha, LT \alpha := (le_refl : \forall a : \alpha, a \leq a) (le_trans : \forall a b c : \alpha, a \leq b \impl b \leq c \impl a \leq c) (lt_iff_le_not_le : \forall a b : \alpha, a &lt; b \iff (a \leq b \and \not b \leq a)) example (\alpha : Type u) [P : MyPreorder \alpha] : P.lt = (\lambda a b : a =&gt; a \leq b \and \not b \leq a) := by funext x y apply propext apply P.lt_iff_le_not_le </code></pre> <p>From this I would say that MyPreorder is just as powerful as a definition as the one in the Mathlib port. What am I overlooking?</p> <p>Interestingly, I've so far not managed to derive the latter from the former. That may just be my own inexperience, or it may be a &quot;typetheoretic thing&quot; that I'm not spotting.</p> <p>Can anyone explain this to me? And is there someone who can derive the latter from the former, perhaps?</p> <p>Many thanks!</p> https://proofassistants.stackexchange.com/q/1747 2 Equality of records with members whose types are dependent (Lean 4) Jozef Mikušinec https://proofassistants.stackexchange.com/users/1695 2022-09-21T18:13:18Z 2022-09-22T23:48:45Z <p>(Previously, I <a href="https://proofassistants.stackexchange.com/q/1740/1695">asked</a> about converting a term <code>a: A</code> to a term of type <code>B</code> provided that <code>A = B</code>. Apologies if this turns out to be (about) the same issue, but I am convinced it's a different one.)</p> <p>Let's say we have a structure like this (the latter example is included for completeness, but I am mainly interested in the propositional case if it makes any difference).</p> <pre><code>-- Example with a proposition structure Interval where lower: Nat upper: Nat lu: lower ≤ upper -- Example with a function structure Signature := symbol : Type arity : symbol → Type </code></pre> <p><strong>Problem</strong>: I would like to prove that for any two intervals <code>a</code> and <code>b</code>, if <code>a.lower = b.lower</code> and <code>a.upper = b.upper</code>, then <code>a = b</code>. (For instance to later define a pointwise partial order on intervals, and prove that it's antisymmetric.)</p> <p>As long as the structure contains no members whose types are dependent, this is a simple matter:</p> <pre><code>structure PreInterval where lower: Nat upper: Nat def PreInterval.eq (a b: PreInterval) (lEq: a.lower = b.lower) (uEq: a.upper = b.upper) : a = b := -- (Can this be done in fewer steps/without the middleman?) let aMid: a = ⟨b.lower, b.upper⟩ := lEq ▸ uEq ▸ rfl; let midB: ⟨b.lower, b.upper⟩ = b := rfl; Eq.trans aMid midB </code></pre> <p>However, this approach fails for members of dependent types (like <code>lu</code>), because their equality cannot be even stated (trying so produces a &quot;type mismatch&quot; error, since they are of different types).</p> <p>Applying the trick from the previous question does not seem to be of help, because it seems to me I don't need to convert one value into a value of the other type, I need to show that they are equal, despite that they have different types. (Or not?)</p> <p>Is this possible? Or should I be doing something else?</p> <hr /> <p><strong>Subquestion</strong>, if anybody knows the history:</p> <p>I've looked around, and it seems to me that in Lean 2, there was the concept of heterogenous equality, exactly for this purpose. It allowed generalizing <code>congr</code> for dependent types, and could even be turned into a proof of regular equality! (Ctrl+F &quot;heq.to_eq&quot; <a href="https://github.com/leanprover/tutorial/blob/master/06_Inductive_Types.org" rel="nofollow noreferrer">here</a>)</p> <p>However, the only mention of heterogenous equality in Lean 4 that I found was in the tutorial <a href="https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html" rel="nofollow noreferrer">chapter 7</a>, which says it will be introduced in the next chapter, but it is not. The source of Lean 4's Prelude <a href="https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L438" rel="nofollow noreferrer">warns against using it</a>, and <code>heq.to_eq</code> seems to not exist anymore. <em>What happended to <code>heq</code>?</em></p> https://proofassistants.stackexchange.com/q/1741 3 Is 'subsingleton elimination' the same concept as 'function comprehension'? ice1000 https://proofassistants.stackexchange.com/users/32 2022-09-19T17:23:29Z 2022-09-26T09:25:41Z <p>I saw:</p> <ul> <li><em>subsingleton elimination</em> from <a href="https://lean-forward.github.io/logical-verification/2018/41_notes.html" rel="nofollow noreferrer">lean-forward</a>, which, I so far understood as &quot;eliminate a type in <code>Prop</code> to a type in whatever universe that we know has at most one constructor with arguments either in <code>Prop</code> or also subsingletons&quot;.</li> <li><em>function comprehension</em> from <a href="https://www.jonmsterling.com/papers/sterling-angiuli-gratzer:2022.pdf" rel="nofollow noreferrer">XTT</a>, <span class="math-container">$\S 8.2.1$</span>, which corresponds to the statement that (paraphrased) if <code>∀ (a : A), ∃ (b : B), R a b ∧ b unique</code>, then <code>∃ f : A -&gt; B</code>, it holds that <code>∀ (x : A), R x (f x)</code>. If <code>A</code> lives in <code>Type</code> then this is trivial, but when <code>A : Prop</code> then this becomes more interesting: we intend to erase propositions, so we cannot have their computational content relevant, so only when we know <code>b unique</code> do we say <code>∀ x, f x = b</code>.</li> </ul> <p>I wonder are these concepts the same thing? Is there any slight difference I didn't notice? They're both about eliminating <code>Prop</code> into some uniquely inhabited <code>Type</code>.</p> https://proofassistants.stackexchange.com/q/1740 10 Given A = B, how to prove a: A` also has type B in Lean 4 Jozef Mikušinec https://proofassistants.stackexchange.com/users/1695 2022-09-17T17:02:33Z 2022-09-20T14:11:50Z <p>I guess my question can be reduced to implementing this function:</p> <pre><code>def abEq (A B : Type) (a: A) (ab : A = B): B := sorry </code></pre> <p>I am new to Lean 4 and started learning from the <a href="https://leanprover.github.io/theorem_proving_in_lean4/title_page.html" rel="noreferrer">official tutorial</a>, currently I am at the chapter 7 (<a href="https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html" rel="noreferrer">Inductive types</a>).</p> <p>I already know that substituting things in propositions given a certain equality is done using <code>Eq.subst</code>, and <code>Eq.subst ab a</code> is among the things I tried. My problem is that the type assertion <code>a: A</code> is not a proposition, and I have no idea how to proceed.</p> <hr /> <h3>Why I am trying to do this</h3> <p>Perhaps I am suffering from an <a href="https://meta.stackexchange.com/questions/66377/what-is-the-xy-problem">XY problem</a>, so I thought including the following might help. In Lean, I am trying to define what I would define in set theory like this:</p> <p>A signature is a pair <span class="math-container">$(Op, ar)$</span>, where</p> <ul> <li><span class="math-container">$Op$</span> is an arbitrary set of operations, and</li> <li><span class="math-container">$ar\colon Op \to Nat$</span> a function giving their arities.</li> </ul> <p>Let <span class="math-container">$Sig_{Op}$</span> be the set of all signatures with <span class="math-container">$Op$</span> as the set of operations, then <span class="math-container">\begin{align} arity\colon Sig_{Op} &amp;\to Op \to Nat \\ (Op, ar) &amp;\mapsto op \mapsto ar(op) \end{align}</span> returns the arity of the operator <span class="math-container">$op$</span> in the signature <span class="math-container">$(Op, ar)$</span>.</p> <p>I came up with this:</p> <pre><code>def signature := (Op: Type) × (Op → Nat) def sigOp (Op: Type) := { s: signature // s.fst = Op } def arity {Op: Type} (op: Op) (s: sigOp Op): Nat := ... </code></pre> <p>but I am stuck implementing the function <code>arity</code>. <code>s.val.snd op</code> does not work, because <code>s.val.snd</code> expects an argument of type <code>s.val.fst</code>, while <code>op</code> has type <code>Op</code>. The value <code>s</code> carries a proof <code>s.property: s.val.first = Op</code>, but I don't know how to apply it. Is my problem in that I just don't know how to implement <code>arity</code>, or are my Lean definitions themselves wrong and I need to change them? If so, how?</p> https://proofassistants.stackexchange.com/q/1738 5 Can we bring unification results under cofibrations outside? ice1000 https://proofassistants.stackexchange.com/users/32 2022-09-17T02:15:51Z 2022-09-17T02:15:51Z <p>Say we have an elaborator which supports metavariables and solve them on flex-rigid cases (with the obvious occurrence checking and scope checking). If we do such unification under a cofibration, do we still get correct results? To put it more formally, when we do something like <span class="math-container">$$\Gamma,\varphi \vdash ~?\equiv v:A$$</span> where <span class="math-container">$?$</span> is a metavariable generated during type checking outside of <span class="math-container">$\varphi$</span>, and <span class="math-container">$v$</span> is a well-typed term of type <span class="math-container">$A$</span>. Can we solve <span class="math-container">$?$</span> to <span class="math-container">$v$</span> and bring the solution to the place where it is generated, which does not have <span class="math-container">$\varphi$</span> in the context?</p> https://proofassistants.stackexchange.com/q/1737 4 Can we completely erase propositions in the type checker? ice1000 https://proofassistants.stackexchange.com/users/32 2022-09-16T16:36:46Z 2022-09-19T11:47:59Z <p>Related question on semantic side: <a href="https://proofassistants.stackexchange.com/q/1183/32">How much of trouble is Lean&#39;s failure of normalization, given that logical consistency is not obviously broken?</a></p> <p>Suppose we have an impredicative universe of strict propositions (as in Lean), which, if we try to compute the terms, it <a href="https://arxiv.org/abs/1911.08174" rel="nofollow noreferrer">may loop</a>.</p> <p>So, I wonder, if we just erase them as some kind of dummy terms in the type checker, would it prevent the loop? An obvious problem comes to my mind is that eliminating a proposition into an ordinary type can be problematic, because we can no longer apply a proposition to a pattern matching or something, because we do not know anything about them except their existence. Is such elimination necessary for usability?</p> https://proofassistants.stackexchange.com/q/1735 3 .CoqMakefile.d required by CoqMakefile but not generated Rincewind https://proofassistants.stackexchange.com/users/1689 2022-09-15T15:23:19Z 2022-09-15T17:18:52Z <p>I am trying to use CoqMakefile to automatically build my Coq project in Coq 8.15.2. When I did this the compilation failed because a file &quot;.CoqMakefile.d&quot; was expected by make but did not exists and make did not know how to produce it. This problem occured on two different computers with two different operating systems.</p> <p>Weirdly, creating an empty file with this name solved the issue and make now runs without a problem. Even more weirdly, deleting the file again did not cause a problem: Now make is able to automatically generate it.</p> <p>I am puzzled. What is going on here? What is the job of .CoqMakefile.d? Why could it not be generated by the automatically generated CoqMakefile? And why can it be generated once it has existed once?</p> https://proofassistants.stackexchange.com/q/1731 1 Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie? CrabMan https://proofassistants.stackexchange.com/users/420 2022-09-14T23:57:37Z 2022-09-16T18:07:24Z <p>In this question, I am talking about the language <a href="https://github.com/the-little-typer/pie" rel="nofollow noreferrer">Pie</a> described in the book <a href="https://thelittletyper.com/" rel="nofollow noreferrer">The Little Typer</a>.</p> <p>One can derive that <span class="math-container">$0=1$</span> is contradictory:</p> <pre><code>(claim 0=1-&gt;Absurd (-&gt; (= Nat 0 1) Absurd)) (define 0=1-&gt;Absurd (λ (0=1) (replace 0=1 (λ (x) (which-Nat x Trivial (λ (x-1) Absurd))) sole))) </code></pre> <p>When I tried to prove that left being equal to right is contradictory in a similar way, I failed:</p> <pre><code>(claim l=r-&gt;Absurd (-&gt; (= (Either Trivial Trivial) (left sole) (right sole)) Absurd)) (define l=r-&gt;Absurd (λ (l=r) (replace l=r (λ (x) (ind-Either x (λ (x) U) (λ (triv) Trivial) (λ (triv) Absurd))) sole ))) </code></pre> <p>The code snippet above fails with an error highlighting <code>U</code> and saying <code>U is a type, but it does not have a type.</code></p> <p><code>Either</code> doesn't have an expression analagous to <code>which-Nat</code> or <code>rec-Nat</code>, it only has <code>ind-Either</code>, and <code>ind-Either</code> requires writing a motive, and a motive can't return <code>U</code> because Pie has only one universe. So, I think <code>which-Nat</code> and <code>rec-Nat</code> are cheats which allow this while <code>Either</code> doesn't have such a cheat and that's why it's impossible to prove <code>(-&gt; (= Nat 0 1) Absurd)</code>. Am I right?</p> <hr /> <p><strong>Update</strong>. Dan Doel has explained in his answer that <code>(-&gt; (= (Either Trivial Trivial) (left sole) (right sole)) Absurd)</code> can be proven by first mapping <code>(Either Trivial Trivial)</code> to <code>0</code> or <code>1</code> and then using congruence with <code>0=1-&gt;Absurd</code>:</p> <pre><code>(claim EitherTrivialTrivial-&gt;Nat (-&gt; (Either Trivial Trivial) Nat)) (define EitherTrivialTrivial-&gt;Nat (λ (x) (ind-Either x (λ (x) Nat) (λ (triv) 0) (λ (triv) 1)))) </code></pre> <p>and then I can do either</p> <p><code>(define l=r-&gt;Absurd (λ (l=r) (0=1-&gt;Absurd (cong l=r EitherTrivialTrivial-&gt;Nat))))</code></p> <p>or</p> <pre><code>(define l=r-&gt;Absurd (λ (l=r) (0=1-&gt;Absurd (replace l=r (λ (x) (= Nat 0 (EitherTrivialTrivial-&gt;Nat x))) (same 0))))) </code></pre> https://proofassistants.stackexchange.com/q/1730 5 Very dependent functions Mike Shulman https://proofassistants.stackexchange.com/users/98 2022-09-14T18:11:47Z 2022-09-21T11:51:49Z <p>A &quot;very dependent function&quot; is a function whose output <em>type</em> at input <span class="math-container">$n$</span> depends on its own output <em>values</em> at inputs <span class="math-container">$k&lt;n$</span>. Is there a precise definition of such things that makes sense in formal dependent type theory (e.g. Martin-Lof Type Theory or the Calculus of Constructions)?</p> <p>The reference everyone points to for very dependent functions is Hickey's <a href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.4169" rel="noreferrer">Formal Objects in Type Theory Using Very Dependent Types</a> (section 3). But it looks to me like he only gives a PER-style semantics, not a syntax that stands on its own. In particular, his definition might be implementable in a NuPRL-like proof assistant (maybe --- I don't know enough about such proof assistants to be sure), but it's not clear to me how it could be implemented in a proof assistant like Agda, Coq, or Lean. Is my reading of Hickey correct? Has anyone ever implemented very dependent functions in a proof assistant based on something like MLTT or CoC?</p> https://proofassistants.stackexchange.com/q/1727 4 How important is global choice (a la Lean, HOL Light, Isabelle/HOL) practically? Jason Rute https://proofassistants.stackexchange.com/users/122 2022-09-11T19:55:47Z 2022-09-24T12:19:17Z <p>Choice is indispensable for much of modern classical mathematics. Therefore, most proof assistants offer it as part of their standard library. The most powerful version is sometimes called global choice or Hilbert's choice operator. This I believe is the version used by Lean, HOL-Light, and Isabelle/HOL, and they use it liberally. In particular, in Lean it is given by:</p> <pre><code>axiom choice {α : Sort*} : nonempty α → α </code></pre> <p>However, in some ways, global choice is maybe a bit too strong. It isn't compatible with univalent foundations and it leads to a strange situation where one can define named functions which are not well-defined such as <em>the function</em> mapping a vector space to <em>its basis</em>.</p> <p>Instead there are two other forms of choice which are more reasonable, unique choice and the axiom of choice.</p> <p>By unique choice (UC), I mean the version which is comparable to Lean's choice operator, but requires a unique element to choose from. I believe it is also called Church's iota operator.</p> <pre><code>axiom unique_choice {α : Sort*} : nonempty α → subsingleton α → α </code></pre> <p>This still allows us to define functions by their properties, as long as we can show only one such function exists. (In many logics, this follows from other axioms.)</p> <p>By the Axiom of Choice (AC) I mean something like this:</p> <pre><code>axiom axiom_of_choice : ∀ (A B : Type) (R : A → B → Prop), (∀ x : A, ∃ y : B, R x y) -&gt; ∃ f : A → B, (∀ x : A, R x (f x)) </code></pre> <p>I may also need to allow <code>B(x)</code> to depend on <code>x : A</code>. (Also, this is the version where we assume all types are sets, in the HoTT sense. More generally, we would restrict <code>A</code> to be a set.)</p> <p><strong>My question is if it is practical to replace global choice with unique choice and the axiom of choice?</strong></p> <p>For example:</p> <ol> <li><strong>Would it be fairly routine to replace global choice in Lean's mathlib, HOL-Light's library, or Isabelle's AFP with the axiom of choice and unique choice?</strong></li> <li><strong>Do practitioners in Coq and other systems where they are more careful with axioms find it easy to do modern classical mathematics with just <code>UC</code> and <code>AC</code>?</strong></li> </ol> <p>For clarification, my question is not about</p> <ul> <li>the pure logical strength of global choice: I don't know the specifics, but I assume there is something that can be proved with global choice and can't with <code>AC + UC</code>. If so, I'm also assuming it isn't particularly mathematically relevant or meaningful. Of course, if I'm mistaken and there is a theorem commonly used in mathlib, AFP or HOL-Light that doesn't have a simple <code>AC + UC</code> provable alternative, I'd love to hear it.</li> <li>pedantry: I might be not stating <code>UC</code> or <code>AC</code> in exactly the way I need or there may be an extra axiom that is needed to go with <code>AC + UC</code> to replace global choice. If so, I'd love to hear it, but please also assume my question assumes that &quot;correct&quot; formulation as well. Nonetheless, I'd only like axioms which roughly follow from both <code>DTT + global-choice</code> and <code>DTT + UA + HIT + AC</code>. (I say roughly, since the my version of AC assumes that all types are sets, whereas a univalent version would be more careful to specify sets explicitly.)</li> <li>constructive math: I'm not asking about removing all choice, just global choice (and replacing it with <code>AC + UC</code>).</li> </ul> <hr /> <p>My motivation for this question is trying to understand how well modern developments of classical formal mathematics can be fit with univalent foundations <a href="https://proofassistants.stackexchange.com/questions/794/what-would-a-fully-classical-and-fully-univalent-itp-and-library-look-like">as in this question</a>. The difference between how one states the axiom of choice seems to be one of the largest differences between say Lean and univalent foundations (but obviously not the only one).</p> https://proofassistants.stackexchange.com/q/1725 1 Does quantification over functions (STLC) increase strength beyond first order logic? Molossus Spondee https://proofassistants.stackexchange.com/users/153 2022-09-11T18:22:28Z 2022-09-14T08:44:01Z <p>Does quantification over functions (STLC) increase strength beyond first order logic?</p> <p>I want to add support for binders in my little constructive first order logic formalism I'm working on but I'm worried allowing functions might make things too powerful.</p> <p>I want to be able to do stuff like axiomize a more constructive version of the image of a set</p> <p><span class="math-container">$$\forall x f y. y \in \{ f(z) \mid z \in x \} \iff \exists z. z \in x \wedge y = f(z)$$</span></p> <p>Or axiomize folding over Peano arithmetic</p> <p><span class="math-container">$$\forall x f. \mu(x, f, \text{O}) = x$$</span> <span class="math-container">$$\forall x f y. \mu(x, f, \text{S}(y)) = f(\mu(x, f, y))$$</span></p> <p>I'm not sure how I want to handle extensionality.</p> <p>Just assume for now</p> <p><span class="math-container">$$(x\colon \Box) \cong y \iff x = y$$</span> <span class="math-container">$$(f\colon \tau_1 \rightarrow \tau_2) \cong g \iff \forall x. f(x) \cong g(x)$$</span></p> <p>Now clearly it's possible to encode quantification over functions in second order logic in a non constructive way using total functional relations.</p> <p>But I'm not sure what it means to encode predicates in terms of the image of a function (defined in terms of the STLC.)</p> <p>I'm not sure what happens if you add an axiom schema for the principle of unique choice either.</p> <p><span class="math-container">$$(\forall x. \exists! y. P(x, y)) \rightarrow \exists! f\colon \tau_1 \rightarrow \tau_2. \forall x. P(x, f(x))$$</span></p> <p>I have heard there are nice systems in between first order logic and second order logic such as monadic second order logic. Maybe a system like monadic second order logic wouldn't be <em>too</em> bad.</p> https://proofassistants.stackexchange.com/q/1722 3 Using proof assistants to generate fast code nicolas https://proofassistants.stackexchange.com/users/1675 2022-09-11T10:09:36Z 2022-09-11T14:00:04Z <p>Proof assistants allow to state that</p> <p><span class="math-container">$$A(BC) = (AB)C$$</span></p> <p>with <span class="math-container">$A$</span>,<span class="math-container">$B$</span>,<span class="math-container">$C$</span> compatible matrices,</p> <p>Is there a formal system that takes this sort of equations to choose among interpretation strategies of some target language, say for evaluation, the one with the lowest cost?</p> https://proofassistants.stackexchange.com/q/1719 3 Equality type and Propositions Topologic https://proofassistants.stackexchange.com/users/1664 2022-09-07T20:10:08Z 2022-09-09T22:22:20Z <p>I'm writing a library in the Lean computer proof assistant.</p> <p>Evidently,</p> <pre><code>X : Type x : X y : X #check x = y </code></pre> <p>Produces &quot;Prop&quot; and not &quot;Type&quot;; propositions are handled within the prop type. Unfortunately, I wanted to actually obtain the pullback of sets like so:</p> <pre><code>X : Type Y : Type Z : Type f : X \rightarrow Z g : Y \rightarrow Z \Sigma (x : X), \Sigma (y : Y) , f(x) = g(y) </code></pre> <p>Since f(x) = g(y) produces a proposition instead of the singleton I'm at a loss to construct the pullback the way I'd like. Is there an alternative to the equality type in Lean which produces instead the singleton? It'd be nice to have a way of constructing maps Prop -&gt; Type, particularly the one sending 1 to * and 0 to empty type.</p> https://proofassistants.stackexchange.com/q/1717 2 Canonical forms of combinators Molossus Spondee https://proofassistants.stackexchange.com/users/153 2022-09-07T17:44:15Z 2022-09-09T05:39:16Z <p>Binders are painful when dealing with metatheory. Combinators are one potential approach to avoid the pain of binders. But it'd be nice if I could normalize combinators to canonical forms. Is there something like hereditary substitution and canonical forms for combinators like SKI or BCKW?</p> <p>The STLC is easy to give canonical forms with a bidirectional style.</p> <pre><code>Inductive type := pt | fn (_ _: pt). Inductive var: list type -&gt; type -&gt; Type := | Z {G A}: var (A :: G) A | S {G A B}: var G A -&gt; var (B :: G) A. Inductive con: list type -&gt; type -&gt; Type := | lam {G A B}: con (A :: G) B -&gt; con G (fn A B) | neu {G}: val G pt -&gt; con G pt with val: list type -&gt; type -&gt; Type := | get {G A}: var G A -&gt; val G A | app {G A B}: val G (fn A B) -&gt; con G A -&gt; val B. </code></pre> <p>But I'm not really sure how you'd do the same sort of thing for combinators.</p> https://proofassistants.stackexchange.com/q/1713 1 Suppressing notation in Lean Topologic https://proofassistants.stackexchange.com/users/1664 2022-09-07T15:06:42Z 2022-09-07T16:27:49Z <p>I'm using the Lean computer proof assistant and customizing some notation. Here's the example I'm working with:</p> <pre><code>def comp (X Y Z : Type*) (g : [Y, Z]) (f : [X, Y]) (x : X) : Z := g (f x) constant X : Type constant Y : Type constant Z : Type constant f : X \rightarrow Y constant g : Y \rightarrow Z def h := comp(X)(Y)(Z)(g)(f) </code></pre> <p>One thing that would be really convenient is being able to omit characters. In the code above, it would be nice if Lean could infer the (X)(Y)(Z) in comp(X)(Y)(Z)(g)(f).</p> <p>So I was hoping that somehow it would be possible for Lean to infer X and Y and Z from g and f. Is this possible?</p> <p>More generally, I am interested in any notation feature in lean which could infer types of things so as to make the notation cleaner for myself.</p> <p>For instance, how do I obtain the type of something for use in further computations. That is, suppose a : A, A : Type. I want to obtain A from a and construct from it the type A \rightarrow A in a closed form involving a.</p> https://proofassistants.stackexchange.com/q/1711 0 Coproducts in Lean Topologic https://proofassistants.stackexchange.com/users/1664 2022-09-06T23:49:49Z 2022-09-08T14:36:42Z <p>All,</p> <p>I am using Lean. I am hoping to obtain a coproduct construction which works something like this:</p> <pre><code>A : Type B : Type COPRODUCT(A, B) : Type a : A \rightarrow C b : B \rightarrow C COPROD(a, b) : COPRODUCT(A, B) \rightarrow C FIRST : A \rightarrow COPRODUCT(A, B) SECOND : B \rightarrow COPRODUCT(A, B) t : COPRODUCT(A, B) \rightarrow C t \circ FIRST = a t \circ SECOND = b </code></pre> <p>Is the easiest way here to use dependent sum over Bool?</p> <p>Note that this follows pretty literally the universal property for coproduct, which is what I'm aiming for.</p> https://proofassistants.stackexchange.com/q/1709 1 Does Agda's --injective-type-constructors flag have canonicity? Ember Edison https://proofassistants.stackexchange.com/users/673 2022-09-06T04:41:49Z 2022-09-07T12:15:18Z <p>Since 2010/01/07, when the <a href="https://sympa.inria.fr/sympa/arc/coq-club/2010-01/msg00007.html" rel="nofollow noreferrer">Anti-classicality of Agda was proved by Chung-Kil Hur</a>, Agda's <code>--injective-type-constructors</code> is separated from the main branch of Agda (making the main branch avoid Anti-classical) and stabilized to its current state.</p> <p>This flag is marked as &quot;possibly inconsistent&quot; and there is a lack of further research and disclosure of the rules.</p> <p>If this flag enjoys canonicity, it would be helpful for studying its consistency.</p> https://proofassistants.stackexchange.com/q/1705 1 Why is the normal form of an ind-Nat expression with a function type an elimination-of-a-function expression CrabMan https://proofassistants.stackexchange.com/users/420 2022-09-04T11:58:39Z 2022-09-15T00:35:14Z <p>In this question, I am talking about the language <a href="https://github.com/the-little-typer/pie" rel="nofollow noreferrer">Pie</a> described in the book <a href="https://thelittletyper.com/" rel="nofollow noreferrer">The Little Typer</a>.</p> <p>Consider the definition</p> <pre><code>(claim foo-or-bar (-&gt; Nat Atom Atom)) (define foo-or-bar (λ (n) (ind-Nat n (λ (n) (-&gt; Atom Atom)) (λ (a) 'foo) (λ (n-1 result_n-1 a) 'bar)))) </code></pre> <p>If I then type <code>foo-or-bar</code> on a separate line and execute, Pie outputs</p> <pre><code>(the (→ Nat Atom Atom) (λ (n x₁) ((ind-Nat n (λ (n₁) (→ Atom Atom)) (λ (a) 'foo) (λ (n-1 result_n-1 a) 'bar)) x₁))) </code></pre> <p>So, Pie says that the second code snippet is the <em>normal form</em> of <code>foo-or-bar</code>. It's pretty clear why</p> <pre><code>(λ (n x₁) ((ind-Nat n (λ (n₁) (→ Atom Atom)) (λ (a) 'foo) (λ (n-1 result_n-1 a) 'bar)) x₁)) </code></pre> <p>is the <em>same</em> <code>(-&gt; Nat Atom Atom)</code> as</p> <pre><code>(λ (n) (ind-Nat n (λ (n) (-&gt; Atom Atom)) (λ (a) 'foo) (λ (n-1 result_n-1 a) 'bar))) </code></pre> <p>It's by <em>The Final Second Commandment of lambda</em>, which says</p> <blockquote> <p>If <code>f</code> is a <code>(Pi ((y Y)) X)</code>, and <code>y</code> does not occur in <code>f</code>, then <code>f</code> is the same as <code>(lambda (y) (f y))</code>.</p> </blockquote> <p>But The Little Typer say that the <em>normal form</em> of an expression is the most direct way of writing it. And, frankly, what I wrote in the definition of <code>foo-or-bar</code> seems more direct than what Pie says its normal form is. So, why is that the normal form? I remember the book said somewhere that if <code>f</code> is a neutral expression of a Pi type, then <code>(lambda (x) (f x)</code> is the normal form of <code>f</code>. This seems similar to the situation with <code>foo-or-bar</code> but not directly applicable.</p> https://proofassistants.stackexchange.com/q/1703 1 Inductive types associated to instances of a structure in Lean Topologic https://proofassistants.stackexchange.com/users/1664 2022-09-03T14:20:33Z 2022-09-04T09:22:30Z <p>I am using the Lean computer proof assistant. I am using the combinatorial structure of a graph with an abelian operation on its edges as a learning example.</p> <p>In it I have a structure Graph. <strong>I want to have several inductive types associated to each particular structure g : Graph</strong>; so that g.edges, g.vertices would or something like that. Then I want - basically, and in pseudocode - the following associated functions:</p> <p>g.head : g.edges -&gt; g.vertices</p> <p>g.tail : g.edges -&gt; g.vertices</p> <p>g.multiplication : {(x, y) : g.vertices x g.vertices // g.tail(y) == g.head(x)} -&gt; g.vertices</p> <p>That's just an example so that people get the point. What I'm saying basically is that I want something which can play the role that a class within a class has in python. Structure is nice for very simple algebraic structures, but I want to be able to nest structures, put types of any kind internal to a structure (much like a class can go in a class in python).</p> https://proofassistants.stackexchange.com/q/1701 -2 A project in Lean which involves "programming" Öölby Görgenöldel https://proofassistants.stackexchange.com/users/1659 2022-09-03T00:54:35Z 2022-09-05T17:30:33Z <p>all,</p> <p>I have a project in Lean which turns out to involve some features which might better be called programming. So, for that part of the project, I was thinking I would treat Lean like it is Python in a few ways. For this I was hoping to have dynamic data types. Could anyone help me by writing out the following examples, translating from pseudocode to Lean? The more explicit the better.</p> <p>Thanks very much!</p> <p><strong>INT: Dynamic natural number type</strong></p> <ul> <li>INT a = 1</li> <li>a = a + 1</li> <li>a = 3</li> </ul> <p><strong>STRING: a dynamic string type</strong></p> <ul> <li>STRING s = &quot;a&quot;</li> <li>s = &quot;b&quot; %Now s is set to &quot;b&quot;</li> </ul> <p><strong>LIST[X]: a dynamic list of type X</strong></p> <ul> <li>l : LIST[STRING] = [&quot;a&quot;,&quot;b&quot;, &quot;c&quot;]</li> <li>l = &quot;k&quot; %resets &quot;a&quot; to &quot;k&quot;. The new list is [&quot;k&quot;, &quot;b&quot;, &quot;c&quot;]</li> <li>l.delete(1) %deletes &quot;b&quot;. The new list is [&quot;k&quot;, &quot;c&quot;]</li> <li>l.add(&quot;b&quot;, 2) %new list is [&quot;k&quot;, &quot;c&quot;, &quot;b&quot;]</li> </ul> <p><strong>STRUCTURE: a dynamic class-ish type</strong></p> <ul> <li>Can introduce any number of pieces of associated types like strings, lists of strings, etc.</li> <li>Can be initiated by specifying associated types</li> <li>Some associated types are default</li> <li>Accessing and modifying associated types</li> <li>Demanding proofs of various properties during initiation</li> </ul> <p><strong>STRUCTURE whose constituents have a product</strong></p> <ul> <li>S : STRUCTURE</li> <li>s1 : S</li> <li>s2 : S</li> <li>a : s1</li> <li>b : s2</li> <li>#check (a, b)</li> </ul> <p>s1 x s2</p> <ul> <li>a : s1 x s2</li> <li>#check pi1(a)</li> </ul> <p>s1</p> <ul> <li>#check pi2(a)</li> </ul> <p>s2</p> <p>Thanks very much for any help!</p> https://proofassistants.stackexchange.com/q/1698 1 Making a finite graph type in Lean - introduction rule Öölby Görgenöldel https://proofassistants.stackexchange.com/users/1659 2022-09-02T13:56:11Z 2022-09-02T19:05:44Z <p>I'm making a finite directed graph type in Lean. I know type theory from an abstract point of view, but I'm struggling to find the way Lean would produce a type playing the role of a &quot;finite set&quot;, where we explicitly specify all of its constituents. I also need to define a type for the incidence preserving functions between different directed graphs. But since types aren't like sets in this way, I'm unsure of what plays this role in Lean.</p> <p>The other thing I'm struggling with is notation. I'd like to be able to introduce a finite graph using something like this: {x, y, z, w, e : x -&gt; y, f : y -&gt; z}. But I'm not sure how flexible Lean's notation is.</p> <p>Thanks so much for any help!</p> https://proofassistants.stackexchange.com/q/1697 0 If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq? with-forest https://proofassistants.stackexchange.com/users/1487 2022-09-02T02:12:38Z 2022-09-02T02:12:38Z <p>From <span class="math-container">$\mathbb{Q}$</span>, the set of all rational numbers, I make some new structure <span class="math-container">$I$</span>, and also make strict order and (equivalence) equality on <span class="math-container">$I$</span>.</p> <p>I want to use rewrite tactic for my defined relations (strict order, or equality). For example,</p> <pre><code>H : a &lt; const_I 0 H0 : const_I 0 == b </code></pre> <p>I want to write</p> <pre><code>rewrite H0 in H. </code></pre> <p>However, this writing tells me that &quot;not a rewritable relation&quot;.</p> <p>Is there a way to use some new defined relations with 'rewrite' tactic?</p> https://proofassistants.stackexchange.com/q/1696 2 Why does an internal term produced by Lean's equation compiler have holes in it? ttbo https://proofassistants.stackexchange.com/users/1608 2022-09-02T01:06:26Z 2022-09-02T20:23:07Z <p>Section 4.7 of the Lean reference manual (version 3.3) gives an example of a division function defined by well-founded recursion. I used the <code>#print</code> command to inspect the internal term that the equation compiler generates, and I found that it has two holes in it. The code below shows the original function, and an internal term that corresponds to it that was produced by the print command (using Lean version 3.48.0).</p> <pre><code>def wfdiv : ℕ → ℕ → ℕ | x y := if h : 0 &lt; y ∧ y ≤ x then have x - y &lt; x, from nat.sub_lt (lt_of_lt_of_le h.left h.right) h.left, wfdiv (x - y) y + 1 else 0 #eval wfdiv 25 6 -- result: 4 -- set_option pp.generalized_field_notation false -- #print wfdiv -- #print wfdiv._main -- #print wfdiv._main._pack def «printed wfdiv._main._pack» : Π (_x : Σ' (ᾰ : ℕ), ℕ), (λ (_x : Σ' (ᾰ : ℕ), ℕ), ℕ) _x := λ (_x : Σ' (ᾰ : ℕ), ℕ), well_founded.fix has_well_founded.wf (λ (_x : Σ' (ᾰ : ℕ), ℕ), psigma.cases_on _x (λ (fst snd : ℕ), id_rhs ((Π (_y : Σ' (ᾰ : ℕ), ℕ), has_well_founded.r _y ⟨fst, snd⟩ → ℕ) → ℕ) (λ (_F : Π (_y : Σ' (ᾰ : ℕ), ℕ), has_well_founded.r _y ⟨fst, snd⟩ → ℕ), dite (0 &lt; snd ∧ snd ≤ fst) (λ (h : 0 &lt; snd ∧ snd ≤ fst), have this : fst - snd &lt; fst, from _, _F ⟨fst - snd, snd⟩ _ + 1) (λ (h : ¬(0 &lt; snd ∧ snd ≤ fst)), 0)))) _x def «printed wfdiv._main» : ℕ → ℕ → ℕ := λ (ᾰ ᾰ_1 : ℕ), «printed wfdiv._main._pack» ⟨ᾰ, ᾰ_1⟩ #eval «printed wfdiv._main» 25 6 -- result: 4 </code></pre> <p>Note that the second <code>#eval</code> shows that <code>«printed wfdiv._main»</code> is still computationally effective even though it has holes in it.</p> <p>The first hole is in the line <code>have this : fst - snd &lt; fst, from _,</code>, and the Lean emacs mode describes it with</p> <pre><code>30:57: don't know how to synthesize placeholder context: _x _x : Σ' (ᾰ : ℕ), ℕ, fst snd : ℕ, _F : Π (_y : Σ' (ᾰ : ℕ), ℕ), has_well_founded.r _y ⟨fst, snd⟩ → ℕ, h : 0 &lt; snd ∧ snd ≤ fst ⊢ fst - snd &lt; fst </code></pre> <p>The second hole is in the line <code>_F ⟨fst - snd, snd⟩ _ + 1)</code>, and the Lean emacs mode describes it with</p> <pre><code>31:43: don't know how to synthesize placeholder context: _x _x : Σ' (ᾰ : ℕ), ℕ, fst snd : ℕ, _F : Π (_y : Σ' (ᾰ : ℕ), ℕ), has_well_founded.r _y ⟨fst, snd⟩ → ℕ, h : 0 &lt; snd ∧ snd ≤ fst, this : fst - snd &lt; fst ⊢ has_well_founded.r ⟨fst - snd, snd⟩ ⟨fst, snd⟩ </code></pre> <p>The <code>&lt;</code> and <code>has_well_founded.r</code> terms both have type <code>Prop</code> when applied to two arguments. Is it correct to say that the equation compiler is omitting these essentially due to &quot;proof irrelevance&quot; (described in section 3.7 of the manual)? In other words, the equation compiler knows that these propositions are true, and also knows that they aren't needed for the actual computation, and so therefore in the code it just leaves them as hypothesized. Is that roughly correct?</p> <p>Assuming that I'm understanding the situation correctly, then I have one more question about this: would the performance of the code be negatively impacted if those holes were filled in? In other words, is the compiler leaving those terms as holes simply because they are computationally irrelevant and so there's no reason to bother filling them in? or is it leaving them as holes because doing so actually improves performance?</p> https://proofassistants.stackexchange.com/q/1694 1 Can I unfold not all things but only one thing in Coq? with-forest https://proofassistants.stackexchange.com/users/1487 2022-09-01T04:35:52Z 2022-09-01T06:19:04Z <p>For example,</p> <pre><code>Example example (a b c : Q) : (a * b) * c == a * (b * c). Proof. unfold Qmult. </code></pre> <p>This code show me this screen.</p> <pre><code>1 goal a, b, c : Q ______________________________________(1/1) Qnum (Qnum a * Qnum b # Qden a * Qden b) * Qnum c # Qden (Qnum a * Qnum b # Qden a * Qden b) * Qden c == Qnum a * Qnum (Qnum b * Qnum c # Qden b * Qden c) # Qden a * Qden (Qnum b * Qnum c # Qden b * Qden c) </code></pre> <p>Can I unfold just one specific multiplication?</p> https://proofassistants.stackexchange.com/q/1689 6 How to implement a visual proof assistant? Molossus Spondee https://proofassistants.stackexchange.com/users/153 2022-08-30T18:55:22Z 2022-09-01T00:35:31Z <p>Higher structures in category theory lead very organically to visual or graphical interpretations in terms of string diagrams and commuting squares. However, it seems hard to implement a graphical calculus or reason about its metatheory.</p> <p>I am aware of prior art like Epigram or Globular but not sure of the state of the art in the area of working with graphical calculi.</p> <p>I feel like the easiest approach to get started might be to export data to external tools like Graphviz but this also feels pretty clumsy and limited.</p> <p>How would I implement and reason about a graphical calculus or proof assistant?</p> https://proofassistants.stackexchange.com/q/1611 8 Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug? Ana Borges https://proofassistants.stackexchange.com/users/113 2022-07-23T11:04:48Z 2022-08-31T22:20:25Z <p>Critical bugs are periodically found in <a href="https://github.com/coq/coq/labels/kind%3A%20inconsistency" rel="noreferrer">Coq</a>, and I assume in other proof assistants as well. We are still happy to mostly trust the proof assistants, partly because these critical bugs are relatively rare, but also because most of the time the bugs are obvious in the sense that it's hard to rely on them without noticing something is off. Or is it? Have there been &quot;proofs&quot; that were later discredited due to such critical bugs?</p> <p>Related: <a href="https://proofassistants.stackexchange.com/questions/1219/has-anyone-ever-accidentally-proven-a-false-theorem-with-type-in-type">this question</a> about type-in-type, which does list some examples of the phenomenon I'm pointing at, although in that case people were knowingly working in an inconsistent setting.</p> https://proofassistants.stackexchange.com/q/1251 12 Learning materials for doing analysis (calculus) in a mechanized way Alex Chichigin https://proofassistants.stackexchange.com/users/333 2022-04-10T13:54:59Z 2022-09-04T16:16:12Z <p>Can we collect (or maybe even write) tutorials and guides on doing analysis in various Proof Assistants? Community wiki style?</p> <hr /> <p>I was reading Lawrence Paulson's blog (highly recommend!) the other week and <a href="https://lawrencecpaulson.github.io/2021/11/17/Cauchy-Schwarz-example.html" rel="noreferrer">https://lawrencecpaulson.github.io/2021/11/17/Cauchy-Schwarz-example.html</a> in particular. It employs pretty specific rules, tactics and theorems relevant to calculus.</p> <p>I have an impression analysis-formalizing libraries for other proof assistants develop some specific tactics and notations too. For instance I looked over <a href="https://github.com/math-comp/analysis/" rel="noreferrer">https://github.com/math-comp/analysis/</a> and <a href="https://github.com/lecopivo/SciLean" rel="noreferrer">https://github.com/lecopivo/SciLean</a></p> <p>So the question is: where can I learn about that specifics?</p> <p>For <em>Program</em> Analysis we have very comprehensive guides like Software Foundations, PLFA, Concrete Semantics and Functional Algorithms, Verified (plus their &quot;fan translations&quot; from one Proof Assistant to another). Do we have (or can we have) anything comparable for <em>Mathematical</em> Analysis?</p> <hr /> <p>A <a href="https://proofassistants.stackexchange.com/questions/256/what-are-good-books-for-learning-about-proof-assistants-for-functional-analysis">related but narrower question</a> was mostly misunderstood and poorly answered as far as I can tell (but decided to mention for completeness).</p>