How does writing proofs in Agda differ from writing them in Isar/Isabelle

automated-theorem-provingconstructive-mathematicsproof-theoryproof-writing

An Isar proof that the square root of 2 is not rational might look like this (according to Wikipedia):

theorem sqrt2_not_rational:
  "sqrt 2 ∉ ℚ"
proof
  let ?x = "sqrt 2"
  assume "?x ∈ ℚ"
  then obtain m n :: nat where
    sqrt_rat: "¦?x¦ = m / n" and lowest_terms: "coprime m n"
    by (rule Rats_abs_nat_div_natE)
  hence "m^2 = ?x^2 * n^2" by (auto simp add: power2_eq_square)
  hence eq: "m^2 = 2 * n^2" using of_nat_eq_iff power2_eq_square by fastforce
  hence "2 dvd m^2" by simp
  hence "2 dvd m" by simp
  have "2 dvd n" proof -
    from ‹2 dvd m› obtain k where "m = 2 * k" ..
    with eq have "2 * n^2 = 2^2 * k^2" by simp
    hence "2 dvd n^2" by simp
    thus "2 dvd n" by simp
  qed
  with ‹2 dvd m› have "2 dvd gcd m n" by (rule gcd_greatest)
  with lowest_terms have "2 dvd 1" by simp
  thus False using odd_one by blast
qed

How would a similar "proof" be written in Agda, given this observation:

Agda doesn’t have the default features for writing classical logic based proofs in contrast to HOL or Isabelle.

I don't have enough knowledge or experience with Proof Assistants, or Agda or Isabelle/Isar to know what this means. I assume it means they have not only a different way of writing the proof, but an entirely different system for proving theorems in Agda than in others like Coq or Isar (Coq uses "tactics", for example). So wondering generally how a proof is written in Agda as contrasted with Isabelle/Isar, using this specific proof as an example. But comparing two other proofs in Isar vs. Agda would also be sufficient. Also, you don't necessarily need to show a proof in Agda. More importantly, I am interested in the general theory of how the two proof systems differ in their model of proofs and their transformation to axioms. It seems that this is an example of how Agda does it:

lemma : (a b : R) → (a + b) · (a + b) ≡ (a · b) + (b · a)
lemma a b =
    begin
    ((a + b) · (a + b)        
    ≡⟨ ·-distr-right a b (a + b) ⟩
    a · (a + b) + b · (a + b)
    ≡⟨ cong₂ _+_ (·-distr-left a a b) (·-distr-left b a b) ⟩
    (a · a + a · b) + (b · a + b · b)
    ≡⟨ cong (_+_ (a · a + a · b)) (cong₂ _+_ refl (alternation b)) ⟩
    (a · a + a · b) +  (b · a + θ)
    ≡⟨ cong (_+_ (a · a + a · b)) (+-θ (b · a)) ⟩
    (a · a + a · b) + (b · a)
    ≡⟨ cong₂ _+_
    (cong₂ _+_ (alternation a) refl)
    refl ⟩
    (θ + a · b) + (b · a)
    ≡⟨ cong₂ _+_ (trans (+-commute θ (a · b)) (+-θ (a · b))) refl ⟩
    (a · b + b · a)
    ∎)

Whereas it seems straightforward in Isabelle/Isar to reason through the "proof" step-by-step, applying rules/tactics to transform a proof "environment" into a final result, I have no idea what is happening in an Agda proof.

Best Answer

The proof you are looking at is just a fancy syntax for basic properties of equations (or preorders, really).

begin is (I believe) an identity function that has very low syntactic precedence, and is just there to look nice.

∎ is another notation for reflexivity, which lets you write T ∎ for a proof of T ≡ T at the end of the proof, to look similar to how some equational proofs might be written.

T ≡⟨ r ⟩ s is a notation for transitivity, where r : T ≡ U and s : U ≡ V. This allows you to write intermediate expressions to keep track of how the various equalities have 'rewritten' the original expression. The syntactic precedence is such that s can be another one of these, so that it looks like multi-step equational reasoning according to rules 'named' by proof terms.

The things inside the brackets are just various equality proof terms. trans is transitivity, refl is reflexivity, cong is for constructing f x ≡ f y from x ≡ y. Etc.

The result is as if you had just composed all the bracketed equality proof terms in order with trans. The operators are just trying to make that somewhat easier to read/understand.

Related Question