Ssreflect Users Discussion List

[<>]

> It really is the same engine -- Coq's type inference engine, namely.
> An Implicit Argument is just one that's automatically replaced by a 
> wildcard 
> before type inference does it's thing. The Unset Strict Implicit directive 
> does help by making the assignment of the Implicit status more reliable: an 
> argument is made implicit when it occurs in the type of another argument 
> (Coq's default uses a complex heuristic to try to determine if the 
> occurrence

> is rigid).

I am a little confused about what is written in Sec 2.5 of the document:
"it enhances the possibilities of using such wildcards."

move/f_p in the following Goal succeeds:

Require Import ssreflect. 
Variable a : nat.
Variable g: nat -> nat -> nat.
Variable p: nat -> Prop.

Axiom f_p: forall a1 a2, p a1 -> p a2 -> p (g a1 2).

Goal p a ->True.
move/f_p. 

Something clever is happening :-)
and I thought I can try to rely on it. 
Is there a complex heuristic behind this behavior which might confuse me?
As my previous example suggests,
I am not working on difficult mathematical proofs.

I am aware that the following script fails. 

Require Import ssreflect. 
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Variable a : nat.
Variable g: nat -> nat -> nat.
(* Variable f: nat -> nat. *)
Variable p: nat -> Prop.

Axiom f_p: forall a1 a2, p a1 -> p a2 -> p (g a1 2).

Goal p a ->True.
move => pa. generalize (f_p pa).  


With best,
Keiko