The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 02/14/2014 07:22 PM, Anders Lundstedt wrote:
> Inductive is_A_formula : Prop ->  Type :=
> | atom_formula P   : is_A_atom P ->  is_A_formula P
> | and_formula  P Q : is_A_formula P ->  is_A_formula Q ->  is_A_formula (P /\ 
> Q).
>
> Definition A_formulas := {P : Prop&  is_A_formula P}.
>
> [...]
>
> (* this is the form I would prefer, this gives "cannot guess decreasing
>     argument of fix". I guess this is caused by the above error *)
> Fixpoint realizes' (a : A) (P : A_formulas) : Prop :=
> let (P, pf) := P in match pf with
> | atom_formula _ _          =>  P
> | and_formula P Q pf_P pf_Q =>  realizes' (p0 a) (existT _ P pf_P) /\
>                                 realizes' (p1 a) (existT _ Q pf_Q)
> end.
>    

Why not just write a helper function with a type like this?
    A -> forall P, is_A_formula P -> Prop
Then you can pattern-match on the 3rd argument without any fuss.