Stream: Beginner Questions

Topic: The different between Lean and Isabelle

Chen Dongheng (Aug 14 2024 at 12:20):

Hi all,
I am a new guy coming from Lean Prover. I want to know whether the usual way we do proving is to give all the subgoals of a proof in the form

  have "..." using "..." by sledgehammer

Compare with Lean, in lean we don't need to give any subgoal of the proof, but just need to use the tactic. After using the tacitc, the remained goals or conditions will change. But when I am using Isabelle, I found that lots of example didn't give the names to these subgoals. It seems that the it has a magic to combine all the conditions and find the proofs.

I want to know what is the correct way to use Isabelle. I am using it to finish the mathematical proofs in MiniF2F (IMO questions)

Mathias Fleury (Aug 14 2024 at 12:36):

Isabelle has both the structured language (Isar) and the unstructured forward backward reasoning (apply-style)

Mathias Fleury (Aug 14 2024 at 12:37):

the structured language is much nicer and much closer to what a human would write and a lot more readable

Mathias Fleury (Aug 14 2024 at 12:38):

Due to the structured language and the better tactics (auto is unmatched), it is less important to name any hypothesis

Mathias Fleury (Aug 14 2024 at 12:38):

because you can usually just let auto figure it auto

Fabian Huch (Aug 14 2024 at 12:40):

And the magic to combine all of the conditions is just unification: Anything you write with show inside a scope will be used to discharge what you have to prove at qed

Chen Dongheng (Aug 14 2024 at 14:44):

Thanks!!!
And I want to know how to use forward reasoning mode in ISAR proof. For example

theory Scratch
  imports Complex_Main
   "HOL-Number_Theory.Cong"
begin

find_theorems name:"mod"

(* lemma 1: Proving that for n >= 2, the last two digits of 5^n are 25. *)
lemma last_two_digits_of_5_power:
  fixes n :: nat
  shows "((5::nat)^(n + 2)) mod (100::nat) = (25::nat)"

proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)

    (* Calculate 5^(n+1) = 5^n * 5 *)
    have temp:"(5^((n::nat) + 1)) = (5^n * (5::nat))"
      by auto
    have "(5^(n + 1)) mod (100::nat) = (5^n * 5) mod (100::nat)"
      using temp by arith

    have h2:"cong (5^(n + 1)) (5^n * 5) 100 "
    by (metis cong_refl power_add power_one_right)

  have h0:"[(25::nat) = (25*5::nat)] (mod (100::nat))"
    by (simp add:cong_def)

  then show ?case
  by (metis (mono_tags, lifting) Suc add_2_eq_Suc' cong_def mod_mod_trivial mod_mult_left_eq power_Suc2)
qed


(* Main theorem: We can now use the lemma to show that 5^2005 mod 100 = 25. *)
theorem mathd_numbertheory_198:
  "(5^2005) mod 100 = (25::nat)"
proof -
  (* Apply the lemma for n = 2005 *)
  have "(5^2005) mod 100 = 25"
    using last_two_digits_of_5_power[of 2005] by (simp add: le_trans)
  (* Conclude the proof *)
  thus ?thesis by simp
qed
lemma mwe: "⟦a = 1+1 ∧ b = 2+1 ∧ c = 3+1 ⟧ ⟹ a = 2 ∧ b = 3 ∧ c = 4"
  apply(simp)
end

I want to know how to change this line into forward reasoning proof

have "(5^2005) mod 100 = 25"
    using last_two_digits_of_5_power[of 2005] by (simp add: le_trans)

Thanks!

Mathias Fleury (Aug 14 2024 at 14:47):

I consider simp to be forward and backward reasoning, as it only applies rewriting.

Mathias Fleury (Aug 14 2024 at 14:47):

Why don't like that proof?

Mathias Fleury (Aug 14 2024 at 14:48):

or to say it differently, what you expect in Lean?

Mathias Fleury (Aug 14 2024 at 14:49):

Ah I see there was a typo in my earlier message: isar is forward (you start with the assumption and go to the goal) while apply is backward (you go from the goal back to things that are true)

Chen Dongheng (Aug 14 2024 at 15:34):

Oh, when I try to write apply-style proof, I often met the error

Illegal application of proof command in "state" mode

I would like to know how many modes are there in Isabelle, and how to change the mode. I just find a easy example to learn how to switch the mode.

Mathias Fleury (Aug 14 2024 at 15:35):

By default (after lemma / have / show / ...) you are in apply mode

lemma mwe: "⟦a = 1+1 ∧ b = 2+1 ∧ c = 3+1 ⟧ ⟹ a = 2 ∧ b = 3 ∧ c = 4"
  apply(simp)
  done

and with proof you switch to Isar mode

Mathias Fleury (Aug 14 2024 at 15:36):

I suggest reading a tutorial on Isabelle like the prog-prove, available in the documentation panel of Isabelle/jEdit

Chen Dongheng (Aug 14 2024 at 15:37):

OK! Thanks. I have read that book, but I didn't get this point.

Last updated: Dec 21 2024 at 16:20 UTC