The Coq mailing list

[Anthony Bordg <bordg.anthony AT gmail.com>]

Hi,

I reproduce here a message that I wrote somewhere else but I didn't get a solution:

I get stuck with the following goal in COQ :

1 subgoal
x : S1
______________________________
________(1/1)
paths
  (concat
     (concat
        (ap (susp_recnd base base (fun _ : Bool => loop))
           (inverse (concat (meridian true) (inverse (meridian false)))))
        loop) loop) loop


Remark that I don't use here display notations so it's easier to see the subterms of the current goal.


I used the following tactic: rewrite (@ap_V  (susp Bool) S1 
(susp_recnd base base (fun _ : Bool => loop)) N N (meridian true @ 
(meridian false)^)).

where ap_V is the following definition in the HoTT library: 

Definition ap_V {A B : Type} (f : A -> B) {x y : A} (p : x = y) :
  ap f (p^) = (ap f p)^
  :=
  match p with idpath => 1 end.

But I have the following error:

Error:
Found no subterm matching "ap (susp_recnd base base (fun _ : Bool => loop))
                             (inverse

  (concat (meridian true)
                                   (inverse (meridian false))))" in the current goal.

I don't understand because it seems clearly a subterm of my current goal and I gave  well-typed arguments to ap_V. Any suggestion ? I precise that I tried "Set Printing Implicit Arguments" however the error remains the same. Thanks for your help.

Best
Anthony