Re: [isabelle] [ForMaRE] Re: Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]



2012-11-22 15:59 Christoph LANGE:
2012-11-02 22:08 Tobias Nipkow:
It may still be a bit simpler to write
"1<=i & i <=n" instead of "in_range n i" - no need to expand in_range. In
general it is a good idea not to invent new constants for existing
concepts:
"in_range n i" is actually the same as "i : {1..n}".
I have now followed your advice; thanks!  Another advantage that is
important to us is that it makes the code more readable.

Overall it helped simplifying my formalisation; however there were some
surprises.

Here is another surprise I forgot to mention. If you or anyone else feel like it, please have a look into the attached file, from which I removed everything else. (Note that the server where I put our whole formalisation will be offline until tomorrow morning.)

In the last case of the case distinction, I would like to infer the fact I call pred_is_component. I need this to continue with the proof.

Now I have been unable to infer pred_is_component directly. But I made it work with a detour via in_range. (So, don't worry, my proof works – it's just not _nice_.)

And when I define in_range as "i : {1..n}" instead "1 <= i /\ i <= n", even that doesn't work.

Cheers,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  2–5 April 2013, Exeter, UK.  Deadlines 10 Dec (stage 1), 14 Jan (st. 2)
  http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/
theory in_range
imports Main Real

begin
type_synonym real_vector = "nat \<Rightarrow> real"

definition in_range ::
  "nat \<Rightarrow> nat \<Rightarrow> bool" where
  "in_range n i \<equiv> 1 \<le> i \<and> i \<le> n"

definition non_negative_real_vector ::
  "nat \<Rightarrow> real_vector \<Rightarrow> bool" where
  "non_negative_real_vector n v \<equiv> \<forall> i::nat . i \<in> {1..n} \<longrightarrow> v i \<ge> 0"

fun maximum ::
  "nat \<Rightarrow> real_vector \<Rightarrow> real" where
  "maximum 0 _ = 0" | (* In our setting with non-negative real numbers it makes sense to define the maximum of the empty set as 0 *)
  "maximum (Suc n) y = max 0 (max (maximum n y) (y (Suc n)))" (* we don't enforce that y is non-negative, but this computation only makes sense for a non-negative y *)

lemma maximum_sufficient :
  fixes n::nat and y::real_vector and m::real
  assumes non_negative: "non_negative_real_vector n y"
    and non_empty: "n > 0"
    and greater_or_equal: "\<forall> i::nat . i \<in> {1..n} \<longrightarrow> m \<ge> y i"
    and is_component: "\<exists> i::nat . i \<in> {1..n} \<and> m = y i"
  shows "m = maximum n y"
    using assms
proof (induct n)
  case 0
  show ?case sorry
next
  case (Suc n)
  (* removed some steps *)
  have "maximum (Suc n) y = m"
  proof (cases "n = 0")
    case True
    show ?thesis sorry
  next
    case False
    show ?thesis
    proof (cases "y (Suc n) = m")
      case True
      show ?thesis sorry
    next
      case False
      (* The following doesn't work:
      with Suc.prems(4) have pred_is_component: "\<exists>k::nat . k \<in> {1..n} \<and> m = y k" by auto
      Therefore we have to use the auxiliary predicate in_range:
      *)
      from Suc.prems(4) have "\<exists>i::nat . in_range (Suc n) i \<and> m = y i"
        unfolding in_range_def by simp
      with False have "\<exists>k::nat . in_range n k \<and> m = y k"
        unfolding in_range_def by (metis le_antisym not_less_eq_eq)
        (* Sledgehammer fails to prove the former when in_range is defined using i \<in> {1..n}; we need the form 1 \<le> i \<and> i \<le> n *)
      then have pred_is_component: "\<exists>k::nat . k \<in> {1..n} \<and> m = y k"
        unfolding in_range_def by simp
      (* OK, we got what we wanted. *)
      show ?thesis sorry
    qed
  qed
  show ?case sorry
qed

end


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.