Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Mutual Fixpoints into mutual inductive types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mutual Fixpoints into mutual inductive types


Chronological Thread 
  • From: Merlin Göttlinger <megoettlinger AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Mutual Fixpoints into mutual inductive types
  • Date: Fri, 05 Jan 2018 11:54:09 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f171.google.com
  • Ironport-phdr: 9a23:/apBMROJOOK/ObUfbIUl6mtUPXoX/o7sNwtQ0KIMzox0LfX6rarrMEGX3/hxlliBBdydt6odzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlViDanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgIOT428mHZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoakYoUIEeUBJ+JYr4j7p1QWrBWmAxWsBP/ryj9JgH/20rM10/48GgzB2QwvAd0OsHPKo9XpKKcSVeG1zK/HzTrddfNbwjj96I3SfRAgpfGAR65/cc3UyUQ2EQ7Ok1ueqYvgPzyP1+QNtXCW7+VhVeKzi24nthp+riKzyccrj4nFno0VylHY9SV53YY6Pse0RFRnbt6jFZtdsTyROYhuQs46XW1kpCI3xqcFtJO7ZiQG1ooryhDFZ/CacYWE/xTuX/uLLzhinnJqYre/ig6y8Ue+zu38UdG50FNQoSpEltnAr3EN1xvP5sSeRPtx40Ws1SuV2wDc7eFEJk80la7FJJI73rEwkZ8TvVzCHi/whkr2kLebels49uWs8ejqYbXrqoWCO4NqhAzyKLkil86iDeggNwgBRWmb+eCy1L35+k35Ra1HjvgonanWt5DVO9gbprK9Aw9U1IYj5AiwDy293dQXmHkINlNFeBadg4f1PFHOJej0De2jjFS0jDdr2/fGM6X9DZXKN3jPiavufbJg60FH0wcz1tBe55dMCr4bOv7zW0nxtMbZDhAjKQC0zfznW51B0dYVXnvKCauEOovTt0WJ76QhObqifogQ7RPwMfwk4cnBE2MlnV4bcqSzlc8SZX+/E+h6J0Sfbnf2qtgEGGYO+AE5Sbq52xW5TTdPaiPqDOoH7TYhBdf+AA==

Pierre Courtieu <pierre.courtieu AT gmail.com> schrieb am Fr., 5. Jan. 2018 um 12:01 Uhr:
2018-01-05 10:29 GMT+01:00 Merlin Göttlinger <megoettlinger AT gmail.com>:
> Hi,
>
> simplified I have the following mutualy inductive type:
>
> Inductive t1 : Set :=
> | a1 : t1
> | a2 {n} : Vector.t t1 n -> t1
> | a3 {n} : Vector.t t2 n -> t1
> with t2 : Set :=
>      | b1 : t2
>      | b2 {n} : Vector.t t1 n -> t2
>      | b3 {n} : Vector.t t2 n -> t2.
>
> I also have two other inductive types:
>
> Inductive t3 : Set :=
> | c1 : t3 -> t3 -> t3
> | c2 {n} : Vector.t t1 n -> t3
> | c3 {n} : Vector.t t2 n -> t3.
>
> Inductive t4 : Set :=
> | d1 : t4
> | d2 : t4 -> t4 -> t4
> | d3 {n} : Vector.t t4 n -> t4
> | d4 {n} : Vector.t t4 n -> t4.

is it really Vector.t t4 n in d3 and d4? Given you comments I would
have expected Vector.t t1 n and Vector.t t2 n.
Yes it is. This datatype represents a more general variant which allows more general arguments for those two "operators". The two fixpoints then transform the arguments into an allowed form (a kind of normal form).

Can you give the function you tried to write? I can't infer it from
what you gave.

Fixpoint f1 f : list t1 :=
  match f with
  | d1 => [a1]
  | d2 x x0 => f1 x ++ f1 x0
  | d3 x => map a2 (VectorUtils.traverse (fun g => f1 g) x)   
  | d4 x => map a3 (VectorUtils.traverse f2 x)
  end
with f2 f : list t2 :=
  match f with
  | d1 => [b1]
  | d2 x x0 => f2 x ++ f2 x0
  | d3 x => map b2 (VectorUtils.traverse f1 x)
  | d4 x => map b3 (VectorUtils.traverse f2 x)
  end.
 
The list part gets handeled in the conversion to t3 but the problem is in defining f1/f2.

VectorUtils.traverse depends on a bunch of stuff I implemented and is the usual operation known from e.g. Haskell with signature G A -> (A -> F B) -> F (G B) where G is (fun T => Vector.t T n) and F is list in my case.

Attatched stripped down versions of all necessary files in a gist for completeness: https://gist.github.com/mgttlinger/a80087e450a1e36963fa3c9cad4794ba


> The problem I'm having is I am trying to convert t4 into t3 (its a kind of
> normalization). The issue comes with handling the cases d3 and d4 which
> corrspond to c2 and c3 respectively. There I essentially need to map a
> function converting to t1/t2 over the vector. Given that t1 and t2 are
> recursive and mutual these functions have to be mutual fixpoints (lets call
> those f1 : t4 -> t1 and f2 : f4 -> t2).
>
> I have played around with this for a while now and I can't get coq to accept
> my definitions for these mutual fixpoints. When I try to map f2 over the
> input vector in the definition of f1, coq produces somewhat strange errors
> like "Not enough arguments" which if i write (fun f => f2 f) turns into a
> complaint that I apply f2 to something which should rather be the whole
> vector (to which it can't even be applied for typing reasons).

Maybe the problem comes more from the fact that your types use
Vector.t in a nested way. Using list would be a problem too.
 It probably does.

Cheers,
Merlin 



Archive powered by MHonArc 2.6.18.

Top of Page