The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Tue, 7 Feb 2012 14:37:45 -0800,
Daniel Schepler 
<dschepler AT gmail.com>
 a écrit :

> On Tue, Feb 7, 2012 at 12:10 PM, AUGER Cédric 
> <Cedric.Auger AT lri.fr>
> wrote:
> 
> > Hello all,
> >  I was thinking on the problem of fixpoint reduction when the
> > argument is a singleton.
> >
> 
> I'm not sure I really understand your proposal.  How would it avoid
> entering an infinite loop when inconsistent axioms or arguments are
> present?  For example, with:
> 
> Inductive non_wf : nat -> nat -> Prop :=
> | non_wf_const : forall n:nat, non_wf (S n) n.
> 
> Fixpoint non_wf_not_wf (n:nat) (Hacc:Acc non_wf n)
>   {struct Hacc} : False :=
> match Hacc with
> | Acc_intro f => non_wf_not_wf (S n) (f (S n) (non_wf_const n))
> end.
> 
> Axiom bad : Acc non_wf 0.
> 
> Corollary contradiction : False.
> Proof.
> exact (non_wf_not_wf _ bad).
> Defined.
> 
> Compute contradiction.

In fact that is a case where I consider
[(non_wf_not_wf _ bad)] not closed (it
depends on the "free variable" [bad]).

And of course, you shouldn't be able to instantiate [bad]
(I know it may be a not so good idea,
 since you couldn't be able to "admit" proofs of well foundness
 to build term and be able to reduce them).

Furthermore, in your example, the recursive call to "non_wf_not_wf"
is under a "match with", so it is already in head normal form; to fit
my examples,

 Fixpoint non_wf_not_wf (n:nat) (Hacc:Acc non_wf n)
   {struct Hacc} : False :=
 non_wf_not_wf (S n) match Hacc with
                     | Acc_intro f => f (S n) (non_wf_const n))
                     end.
would have been better; and shows a case where a fixpoint is a direct
application to itself (and thus breaking one of the comments on my
previous mail), but in fact, I don't see any case where you can define
fxpoints from non empty types to non empty types (in a consistent
environment) which is defined by a direct call to itself applied to
some wisely chosen parameters. I guess it is not possible, since it
seems such functions would be endlessly reduceable.


> 
> On a somewhat related note, I've been wondering whether it would be
> possible to add a reduction of
> 
> match (match a with
>            | const1 => expr1
>            | const2 => expr2
>            end) with
> | const1' => expr1'
> | const2' => expr2'
> end
> 
> to
> 
> match a with
> | const1 => match expr1 with
>   | const1' => expr1'
>   | const2' => expr2'
>   end
> | const2 => match expr2 with
>   | const1' => expr1'
>   | const2' => expr2'
>   end
> end.
> 
> I tend to see nested matches of the first form a lot when applying
> Compute to proofs built using tactics, and in a lot of those cases I
> think a reduction like this would make the end result easier to read
> (especially if expr1 and expr2 are already applications of
> constructors).  By itself, that reduction shouldn't cause problems
> with termination since each one reduces a "nestedness of match"
> measure -- but I'm not sure how it might interact with other
> reductions.

I never thought of that, it seems interesting, and I guess the
forgotten "as _ in _ return _" won't be problematic either.

The only badpoint I see (but only for the user side, not for the
theoretical side), is that it may lead to a (small) explosion in size.
That is if your biggest inductive has 'N' constructors, then the
resulting term can be 'N' times bigger.

Now, assume 'a' 'expr1' 'expr2' are of type 'Ascii.ascii' then you may
transform a term containing 2×256 cases to a term containing 256×256
cases (assuming 'expr1' and 'expr2' contain opaque terms, so that you
cannot reduce them). I know that in practice it should not happen, but
sometimes we are happy to be able to do ugly things.

I don't remember in my experience if you case of "match (match … with…)
with…" occurs often, I think that you more often have "match f (match …
with…) with…". So maybe your idea could be extended to a:

> match f (match a with
>            | const1 => expr1
>            | const2 => expr2
>            end) with
> | const1' => expr1'
> | const2' => expr2'
> end
> 
> to
> 
> match a with
> | const1 => match f expr1 with
>   | const1' => expr1'
>   | const2' => expr2'
>   end
> | const2 => match f expr2 with
>   | const1' => expr1'
>   | const2' => expr2'
>   end
> end.

(ie. put the "f" deeper; but here again, we can get very quite big
terms if there are a lot of cases)