The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

On Fri, 23 Dec 2022 at 01:36, Marko Doko <m.doko AT hw.ac.uk> wrote:

mukesh tiwari wrote:
> how did you figure out ‘ go_app_stated_nicely’? Is there any theory behind it or just experience? (I generally,m avoid let in or match with syntax in proofs, but it seems they are very helpful)

The "nicely" is not about the pattern matching. This is perfectly fine too:

   Theorem go_app_nice_variant_1:
     ∀ (z : A) (xs ys zs : list A),
     (ys, zs) = go z xs → Permutation (ys ++ zs) xs.
   Proof.
     induction xs; simpl; intros.
     * inversion H; trivial.
     * destruct (go z xs) as [ys' zs'].
       destruct (R a z); inversion H; simpl; subst;
         eauto using Permutation_cons, Permutation_sym, Permutation_cons_app.
   Qed.

   Theorem go_app :
       ∀ (xs ys zs : list A) (z : A),
       In z xs ->
       (ys, zs) = go z xs -> Permutation (ys ++ zs) xs.
   Proof.
     intros xs ys zs z IN EQ.
     eapply go_app_nice_variant_1; eauto.
   Qed.


Or this:

   Theorem go_app_nice_variant_2:
     ∀ (z : A) (xs : list A), Permutation ((fst (go z xs)) ++ (snd (go z xs))) xs.
   Proof.
     induction xs; simpl; [trivial | ].
     destruct (go z xs) as [ys' zs'].
     destruct (R a z); simpl;
       eauto using Permutation_cons, Permutation_sym, Permutation_cons_app.
   Qed.

   Theorem go_app :
       ∀ (xs ys zs : list A) (z : A),
       In z xs ->
       (ys, zs) = go z xs -> Permutation (ys ++ zs) xs.
   Proof.
     intros xs ys zs z IN EQ.
     rewrite surjective_pairing in EQ; inversion EQ; subst.
     eapply go_app_nice_variant_2; eauto.
   Qed.


The point is that the assumption (In z xs) is redundant, and I wanted to avoid dragging it along in the induction proof :-)

Ah, now I see my mistake :) (It was a copy paste mistake because the lemma I was trying to prove was  forall (xs ys zs : list A) (z : A),  In z xs -> (ys, zs) = go xs -> List.length zs < List.length xs). Thanks again Marko! 

Best,

Mukesh

Look at the three (equivalent) versions of the theorem I stated:
   * go_app_nice_variant_1 follows your way of stating the theorem.
     This is probably the best formulation for use in proofs, especially
     with proof automation in mind. The drawback is that there are now
     two extra quantified variables and the extra assumption
     ((ys, zs) = go z xs) needs to be stated. All good for Coq, but it
     might be slightly confusing for a human reading the statement.
   * go_app_stated_nicely avoids extra quantified variables and the extra
     equality assumption by using pattern matching to name the components
     of (go z xs).
   * go_app_nice_variant_2 avoids having extra quantified variables by
     using the projection functions to extract the compomnents of (go z xs).

In the end, which of the three approaches above will you take depends on your coding style and how you intend to use the theorem in the future. Oftentimes it turns out having multiple syntactic variants of semantically the same statement is technically very helpful since different statements can fit better in different situations when writing proofs in Coq.


--
Marko


________________________________

Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With campuses and students across the entire globe we span the world, delivering innovation and educational excellence in business, engineering, design and the physical, social and life sciences. This email is generated from the Heriot-Watt University Group, which includes:

  1.  Heriot-Watt University, a Scottish charity registered under number SC000278
  2.  Heriot- Watt Services Limited (Oriam), Scotland's national performance centre for sport. Heriot-Watt Services Limited is a private limited company registered is Scotland with registered number SC271030 and registered office at Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS.

The contents (including any attachments) are confidential. If you are not the intended recipient of this e-mail, any disclosure, copying, distribution or use of its contents is strictly prohibited, and you should please notify the sender immediately and then delete it (including any attachments) from your system.