The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

To answer your second question, Coq's higher order unification
machinery isn't all that great (at least in my admittedly limited
experience), "making the link" depends on this: hence the "return"
annotation.  Improvements to the inference engine are routine updates
to Coq, but all solutions will be heuristic, since in general higher
order unification is undecidable.

Kris


On Wed, Jul 3, 2013 at 1:19 PM, Ilmārs Cīrulis 
<ilmars.cirulis AT gmail.com>
 wrote:
> Thank you very much! Your example works.
> Now I'm going to read Chlipala's book - it's "have to" because this working
> code is for me like mysterious magic.
>
> What are reasons that doesn't allow to write like I wanted? Coq doesn't
> understand something (can't make the link between m and m') - okay, but
> can't it be made more clever? Or is it impossible (or simply bad idea)
> because it will broke something important?
> (I'm little bit sad because Coq doesn't understand very natural way, imo, to
> write this Fixpoint.)
>
>
>
>
> On Wed, Jul 3, 2013 at 1:38 AM, AUGER Cédric 
> <sedrikov AT gmail.com>
>  wrote:
>>
>> Le Wed, 3 Jul 2013 00:28:48 +0300,
>> Ilmārs Cīrulis 
>> <ilmars.cirulis AT gmail.com>
>>  a écrit :
>>
>> > For example, the second way doesn't work.
>> >
>> > Definition ttt (m n:nat) (p: (S m)<=n): m<=n.
>> > Proof. apply le_S_n. inversion p; auto. Qed.
>> >
>> > Fixpoint example (m n:nat) (p: m<=n): list nat :=
>> > match m with
>> > | O => nil
>> > | S m' => cons m (example m' n (ttt m' n p))
>> > end.
>> >
>> >
>> > It gives similar error as before:
>> >
>> > Error:
>> > In environment
>> > example : forall m n : nat, m <= n -> list nat
>> > m : nat
>> > n : nat
>> > p : m <= n
>> > m' : nat
>> > The term "p" has type "m <= n" while it is expected to have type "S
>> > m' <= n".
>> >
>> >
>> > So I suppose that I didn't keep the link between <m> and <m'> good
>> > enough. Any ideas how to do it?
>> >
>>
>> Sorry, I did not have coqtop when I wrote this mail.
>>
>> Have you tried:
>>
>> Fixpoint example (m n:nat) : m<=n → list nat :=
>> match m as m' return m'<=n → list nat with
>> | O => fun p => nil
>> | S m' => fun p => cons m (example m' n (ttt m' n p))
>> end.
>>
>> The thing is that you have "m" in your "p" argument, so you must also
>> destruct m inside of p.
>>
>>
>> >
>> >
>> >
>> > On Tue, Jul 2, 2013 at 5:44 PM, Ilmārs Cīrulis
>> > <ilmars.cirulis AT gmail.com>wrote:
>> >
>> > > Can you copy-paste an example of working code, please? Because I
>> > > still have same problems. :(
>> > > I tried it in both ways and both didn't work.
>> > >
>> > >
>> > > On Tue, Jul 2, 2013 at 4:02 PM, Cedric Auger 
>> > > <sedrikov AT gmail.com>
>> > > wrote:
>> > >
>> > >> You just have to keep the link between «m» and «m'» (Coq forgets it
>> > >> unless you use tricky annotations in the match).
>> > >> For instance, the following should work:
>> > >>
>> > >>
>> > >> Fixpoint example (m n: nat) (p: m<=n): list nat :=
>> > >> match m with
>> > >> | O => nil
>> > >> | S m' => cons m (*or «S m'»*) (example m' n (ttt (S m') n p))
>> > >> end.
>> > >>
>> > >> Someone suggested to have:
>> > >>
>> > >> Theorem ttt (m n:nat) (p: S m<=n): m <= n.
>> > >>
>> > >>
>> > >> That would be even better, as you could write:
>> > >>
>> > >> Fixpoint example (m n: nat) (p: m<=n): list nat :=
>> > >> match m with
>> > >> | O => nil
>> > >> | S m' => cons m (*or «S m'»*) (example m' n (ttt m' n p))
>> > >> end.
>> > >>
>> > >>
>> > >>
>> > >> 2013/7/2 Ilmārs Cīrulis 
>> > >> <ilmars.cirulis AT gmail.com>
>> > >>
>> > >>> Apologies to Pierre Casteran for accidentally answering to his
>> > >>> email.
>> > >>>
>> > >>>
>> > >>> ---------- Forwarded message ----------
>> > >>> From: Ilmārs Cīrulis 
>> > >>> <ilmars.cirulis AT gmail.com>
>> > >>> Date: Tue, Jul 2, 2013 at 11:36 AM
>> > >>> Subject: Re: [Coq-Club] Problems when writing function from proof
>> > >>> to proof.
>> > >>> To: Pierre Casteran 
>> > >>> <pierre.casteran AT labri.fr>
>> > >>>
>> > >>>
>> > >>> Here's example of what I want to make.
>> > >>>
>> > >>> Theorem ttt (m n:nat) (p: m<=n): (pred m) <= n.
>> > >>>> Proof. destruct m. assumption. simpl. apply le_S_n. inversion p;
>> > >>>> auto. Qed.
>> > >>>>
>> > >>>> Theorem _3_14: 3<=14. repeat constructor. Qed.
>> > >>>> Eval simpl in (ttt 3 14 _3_14).
>> > >>>>
>> > >>>> Fixpoint example (m n: nat) (p: m<=n): list nat :=
>> > >>>> match m with
>> > >>>> | O => nil
>> > >>>> | S m' => cons m (example m' n (ttt m n p))
>> > >>>> end.
>> > >>>>
>> > >>>
>> > >>> Function example has error that I want to fix:
>> > >>>
>> > >>>> In environment
>> > >>>> example : forall m n : nat, m <= n -> list nat
>> > >>>> m : nat
>> > >>>> n : nat
>> > >>>> p : m <= n
>> > >>>> m' : nat
>> > >>>> The term "ttt m n p" has type "pred m <= n" while it is expected
>> > >>>> to have type
>> > >>>> "m' <= n".
>> > >>>>
>> > >>>
>> > >>>
>> > >>> On Mon, Jul 1, 2013 at 7:42 PM, Pierre Casteran <
>> > >>> pierre.casteran AT labri.fr>
>> > >>>  wrote:
>> > >>>
>> > >>>> Hi,
>> > >>>>
>> > >>>>   I don't understand what you want exactly to get.
>> > >>>>   By Coq's typing rules, a proof of pred 3 <= 14 is
>> > >>>> ***already*** a proof of 2 <=14.
>> > >>>>
>> > >>>>
>> > >>>> Theorem ttt (m n:nat) (p: m<=n): (pred m) <= n.
>> > >>>> Proof.
>> > >>>>  destruct m. assumption. simpl. apply le_S_n. inversion p; auto.
>> > >>>> Qed.
>> > >>>>
>> > >>>>
>> > >>>> Require Import Arith.
>> > >>>>
>> > >>>> Example E1 : 3 <= 14.
>> > >>>> auto with arith. Qed.
>> > >>>>
>> > >>>> Check ttt _ _ E1 : 2 <= 14.
>> > >>>>
>> > >>>>
>> > >>>>
>> > >>>> Pierre
>> > >>>>
>> > >>>>
>> > >>>>
>> > >>>>
>> > >>>> Quoting Ilmārs Cīrulis 
>> > >>>> <ilmars.cirulis AT gmail.com>:
>> > >>>>
>> > >>>>  I tried to make function (?) that's transforming proof of m<=n
>> > >>>> to
>> > >>>>> proof of
>> > >>>>> (pred m)<=n.
>> > >>>>>
>> > >>>>> My try was:
>> > >>>>> Theorem ttt (m n:nat) (p: m<=n): (pred m) <= n.
>> > >>>>> Proof.
>> > >>>>>  destruct m. assumption. simpl. apply le_S_n. inversion p; auto.
>> > >>>>> Qed.
>> > >>>>>
>> > >>>>> But it always gives proof of (pred m)<=n. For example, proof of
>> > >>>>> 3<=14 is
>> > >>>>> transformed to (pred 3)<=14. I don't know how to simplify it to
>> > >>>>> 2<=14 (using the same function).
>> > >>>>>
>> > >>>>> Is it possible?
>> > >>>>>
>> > >>>>
>> > >>>>
>> > >>>>
>> > >>>>
>> > >>>
>> > >>>
>> > >>
>> > >>
>> > >> --
>> > >> .../Sedrikov\...
>> > >>
>> > >
>> > >
>>
>