[Agda] Positivity checker

[Dan Licata]

What about using an inductive view of the recursive family, so you can
pattern-match on the constructors for the view, rather than
pattern-matching on the indices directly?

  data Nat : Set where
    Zero : Nat
    Succ : Nat -> Nat

  data Base   : Set where base : Base
  data Step A : Set where step : (A -> A) -> Step A
  
  D : Nat -> Set
  D Zero    = Base
  D (Succ n) = Step (D n)  

  -- a one-level view
  data DataView : Nat -> Set where
    BaseV : DataView Zero
    StepV : forall {n} -> (D n -> D n) -> DataView (Succ n)

  -- define the view by pattern-matching on the index
  view : forall {n} -> D n -> DataView n
  view {Zero} base = BaseV
  view {Succ n} (step f) = StepV f

  -- note that n has been refined in the holes
  example : {n : Nat} -> D n -> D n
  example d with (view d)
  ...    | BaseV = {! !}
  ...    | (StepV f) = {! !}

-Dan


On Dec09, Ulf Norell wrote:
> On Tue, Dec 9, 2008 at 12:56 PM, Peter Dybjer <peterd at chalmers.se> wrote:
> 
> >
> > On Dec 8, 2008, at 10:10 AM, Nils Anders Danielsson wrote:
> >
> >>
> >>> The reason why this data type is ok, is because it is isomorphic to the
> >>> corresponding family defined by induction on n.
> >>> But what is the induction principle? Except induction on n?
> >>>
> >>
> >> Do you suggest that one could inadvertently introduce new (stronger)
> >> induction principles by accepting this type (or similar types)?
> >>
> >
> > It depends on what the termination checker would do when pattern matching
> > on this data type. But my feeling is that there is no natural induction
> > principle associated with this type, except induction on n.
> 
> 
> The termination checker accepts functions of the form
> 
> foo base = ...
> foo (step f) = ... foo (f d) ...
> 
> for arbitrary d's. It doesn't care that d happens to have the same type has
> the argument we're recursing over. Formulating that as an induction
> principle you end up with
> 
> elim-D : (P : {n : Nat} -> D n -> Set) ->
>          P base ->
>          ({n : Nat}{f : D n -> D n} ->
>            ((d : D n) -> P (f d)) -> P (step f)) ->
>          {n : Nat}(d : D n) -> P d
> 
> which is easily proved by induction on n:
> 
> data Base   : Set where base : Base
> data Step A : Set where step : (A -> A) -> Step A
> 
> D : Nat -> Set
> D zero    = Base
> D (suc n) = Step (D n)
> 
> elim-D : (P : {n : Nat} -> D n -> Set) ->
>          P base ->
>          ({n : Nat}{f : D n -> D n} ->
>            ((d : D n) -> P (f d)) -> P (step f)) ->
>          {n : Nat}(d : D n) -> P d
> elim-D P b s {zero }  base    = b
> elim-D P b s {suc n} (step f) =
>   s \d -> elim-D P b s (f d)
> 
> / Ulf

> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda