The Coq mailing list

[Bruno Barras <barras AT bergerac.inria.fr>]

  Bonjour,

> J'ai un pb que j'ai pu resoudre mais je ne comprends pas pourquoi
> ca ne marche pas. Peut-etre est-ce du aux types dependants ?
...
> Lemma Ackor_false_fth:(l:(d_list bool four))
>   (Ackor l)=false->(Fth_of_l4 l)=false.
> (Intros l; Elim (non_empty l); Intros x H; Elim H; Clear  H;
>  Intros X H; Rewrite -> H).
> (Unfold Ackor; Unfold Fold_with_f; Simpl).
> (Unfold Fth_of_l4; Simpl).
> 
> (*************** POURQUOI l'elimination suivante (sur un booleen)
>                  ne marche pas ? ************)
> (** Elim (d_Head (d_tl (d_tl X))) **)

Il s'agit en fait d'un problème avec les implicites. Les arguments
implicites sont juste une facilité de syntaxe, mais en représentation
interne, Coq manipule effectivement les arguments synthétisés. Pour
voir ce qui se passe, je vais écrire les termes en donnant certains
de leurs arguments implicites.
Donc, on se trouve dans un but qui est

   (orb x
     (orb (d_Head X) (orb (d_Head (d_tl X))
(!d_Head bool (0) (!d_tl bool (2) (!d_tl bool (3) X))))))
    =false->(d_Head (d_tl (d_tl X)))=false

Or, les arguments implicites de (d_Head (d_tl (d_tl X))) sont résolus
de la façon suivante:
(!d_Head bool (0) (!d_tl bool (pred (3)) (!d_tl bool (3) X)))
                              ^^^^^^^^^^
En effet, le type inféré de (!d_tl bool (3) X) est (d_list A (pred (3)))


Comme la tactique Elim commence par faire Pattern sur ce terme,
l'abstraction ne se fait pas bien et (d_Head (d_tl (d_tl X))) n'est
pas remplacé par true ou false.

Pour s'en sortir, on peut utiliser la tactique Change pour mettre le
but sous une forme qui permettra l'abstraction. Il suffit de faire
Change avec le but courant (tactique que l'on aurait pû croire
sans effet!):

Change (orb x
         (orb (d_Head X)
           (orb (d_Head (d_tl X)) (d_Head (d_tl (d_tl X))))))=false
        ->(d_Head (d_tl (d_tl X)))=false.

Cela a pour effet de rendre les arguments invisibles égaux à ceux qui
seront inférés ultérieurement (c'est-à-dire (pred (3)) au lieu de
(2)). On peut alors faire le Elim.
L'exemple similaire suivant montre comment tromper Pattern, en
réduisant les termes cachés.

Goal (X:(d_list bool (3)))(d_Head (d_tl (d_tl X)))=true.
Intro.
Pattern (d_Head (d_tl (d_tl X))). (* Ce Pattern réussit *)
Undo.
Unfold pred.              (* Il y a en fait un pred caché *)
Pattern (d_Head (d_tl (d_tl X))). (* Ce Pattern échoue *)


Je reconnais que ce n'est pas une solution très
élégante. Malheureusement, je ne vois pas comment on pourrait
exterminer ce problème lié à l'implantation des implicites. Il me
semble que le mieux que l'on puisse proposer actuellement est une 
commande affichant le but avec ses arguments implicites.

Amicalement,

-- 
Bruno Barras
  tel : +33 1 39 63 53 16
  
mailto:Bruno.Barras AT inria.fr
  http://pauillac.inria.fr/~barras