The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

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\...
> >>
> >
> >