Re: [isabelle] intro rule for &&&



On Thu, 20 Dec 2012, John Wickerson wrote:

When I type...

lemma assumes "A ∧ B" shows "A" "B"
using assms
apply rule

...I obtain the following proof state...

goal (2 subgoals):
 1. A ⟹ B ⟹ A
 2. B

... which is insoluble. I think the "apply rule" step is using the conjE rule. Which rule should I apply in order to obtain the preferred proof state below? I briefly tried conjunctionI but that doesn't seem quite to fit.

goal (2 subgoals):
 1. A ⟹ B ⟹ A
 2. A ⟹ B ⟹ B

By the way, I know I can solve this lemma via auto; my question is pedagogical rather than practical.

Automated tools are indeed obstructing the understanding how formal proof really works. Here is my version of the above example:

notepad
begin

  assume ab: "A & B"
  from ab have A and A
    apply rule
     apply assumption
    using ab
    apply rule
    apply assumption
    done

  from ab obtain A and B ..

end


General notes on it:

  * 'notepad' is better for experimentation than old-fashioned 'lemma',
    because it gives you the full proof language.  In top-level theorem
    statements your possibilities to indicate proof structure are more
    limited and one has to simulate things, and obscure the main points
    more than necessary.  There is also the initial goal hanging around,
    but proof is not primarily about goals.

  * The fact "ab" (or your assms) need to be eliminated twice to work on
    the two goals "A" and "B".  The "rule" method implicitly refers to
    conjE, but it works on the head goal only.  Note that in old-fashioned
    tactical reasoning, you would simulate a local fact like "ab" via some
    goal premise "A & B ==> ...", and "apply (erule conjE)" would consume
    that, and the result would indeed become insoluble as you've said.
    In proper Isar, the context grows monotonically, and things can be
    used again as required.

  * My second proof above via 'obtain' does the elimination of fact "ab"
    in a single step, saying that it is possible to assume A and B
    simultaneously thanks to the (implicit) conjE rule.  Recall that ".."
    abbreviates "by rule" (actually "by default", which is a bit more).

    Formally, there is only one goal behind 'obtain', so it works in a
    single rule application step, not two.  It would be more awkward to
    prove:

      from ab have A and B sorry

    which are two goals again.

    Since the context of assumptions is commutative, you may swap the
    obtain result in-place like this:

      from ab obtain B and A ..


Putting it all together, here is my canonical starter proof for Isar:

  assume "A & B"
  then obtain B and A ..
  then have "B & A" ..

You can also make implicit rules explicit like this:

  assume "A & B"
  then obtain B and A by (rule conjE)
  then have "B & A" by (rule conjI)

Using the projections conjD1/conjD2 instead, it becomes a bit more awkward and artificial:

  assume ab: "A & B"
  from ab have a: A by (rule conjD1)
  from ab have b: B by (rule conjD2)
  from b and a have "B & A" by (rule conjI)

To be more fair, here is another variant that minimizes the spaghetti of fact references:

  assume "A & B"
  then have B ..
  from `A & B` have A ..
  with `B` have "B & A" ..

I usually prefer the first-class support of eliminations in Isar via 'obtain' to reduce the formal noise and expose the reasoning more directly.


	Makarius


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