The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

I believe it relates to how delta reduction is implemented in Coq 8.6. Following slightly easier code also fails:

  match goal with
  | H : forall n : ?T, @?x n |- _ =>
    match x with
    | fun n : T => ?b =>
      let not_n := fresh in
      let b''' :=
          constr:(
            fun n : T =>
              match b with
              | not_n =>
                ltac:(let b' := (eval cbv delta in not_n) in
                      exact b')
              end) in
      idtac b''';
      let tH' := eval cbn beta in (forall n : T, b''' n) in
          let tH := type of H in
          change tH with tH' in H
    end
  end.

from debugger, the stack overflow was clearly thrown from the eval line. If we replace delta with "beta iota zeta", there won't be stack overflow. To this point, I believe I can conclude that the the delta reduction and this work around is hitting some weird issue on implementation side. I am wondering if there can be some expert on implementation side can give some hint on what could possibly happen from OCaml?

Unfortunately I am not quite able to provide an easy reproduction for now as it gets stuck in the middle of a project that I am working on. However, the context where it fails has only one dependent implication that is not too deep. In fact, when I call `cbv in Hthe_implication` from proof mode, it does not fail at all. If a hint is given, I would be able to get to debugging on my side.

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
Sent: April 9, 2018 3:15:27 PM
To: ikdc; coq-club AT inria.fr
Subject: Re: [Coq-Club] Unfolded not cannot be refolded

 

Thank you ikdc, this tactic does work.

However, it seems in some situations, it will cause stack overflow. I've got no idea how to quantify "situations" here, but I am looking further to see why it's happening.

Sincerely Yours,

Jason Hu

---

From: ikdc <ikdc AT mit.edu>
Sent: March 30, 2018 11:04:40 PM
To: coq-club AT inria.fr; Jason -Zhong Sheng- Hu
Subject: Re: [Coq-Club] Unfolded not cannot be refolded

 

On 03/28/2018 06:39 PM, Jason -Zhong Sheng- Hu wrote:
> Hi all,
>
>
> Please consider following code:
>
>
> Goal (forall n : nat, ~ (n >= 0) -> False) -> True.
>    unfold not. fold not.
>
> This code unfolded not, so the goal becomes
>
>
> (forall n : nat, (n >= 0 -> False) -> False) -> True
>
>
> But the next one fold not is not able to refold the not to turn the inner condition back to ~ (n >= 0).
>
>
> In general, I tried to write code like this,
>
>
>    intros.
>    match goal with
>    | [ _ : forall _, ?T |- _ ] =>
>      idtac T
>    end.
>
> following the program above, in my Coq 8.6, it says no matching clause. But I suspect this error message is bogus, the real error should be Coq wouldn't allow us to capture a dependent right hand side of implication, due to the potential misuse of free variables. That probably also explains why fold cannot undo what unfold has done.
>
>
> This is especially disturbing, when I do autounfold in *. There are many lemmas expressed with the presence of not, and if not is unfolded, auto family does not seem work well with that form anymore. Might I ask how do you guys handle it?
>
>
> In general, is there a way to manipulate dependent rhs of implication?
>
>
> Sincerely Yours,
>
> Jason Hu
>
>

(* I found the problem interesting, so I decided to take a stab at it.
  * First, I tried using setoid_rewrite. *)

Require Import Coq.Classes.Morphisms.
Require Import Setoid.
Local Existing Instance eq_subrelation | 5.

Goal (forall n : nat, ((n >= 0) -> False) -> False) -> True.
   intro.
   (* H : forall n : nat, (n >= 0 -> False) -> False *)
   assert (forall P : Prop, (P -> False) = ~P) as E by reflexivity.
   setoid_rewrite E in H.
   (* H : forall n : nat, ~ (n >= 0 -> False) *)
   Fail setoid_rewrite E in H. (* why? *)
Abort.

Goal (forall n : nat, ((n >= 0) -> False) -> False) -> True.
   intro.
   (* H : forall n : nat, (n >= 0 -> False) -> False *)
   assert (forall P : Prop, (P -> False) = ~P) as E by reflexivity.
   setoid_rewrite E in H at 2.
   (* H : forall n : nat, ~ n >= 0 -> False *)
   setoid_rewrite E in H.
   (* H : forall n : nat, ~ ~ n >= 0 *)
Abort.

(* However, I found that this only worked if it rewrote in a certain order.
  * I don't know why the second rewrite fails.
  * Hopefully someone can give an explanation or a way to make it work *)

(* Using an idea from Jason Gross in
<https://github.com/coq/coq/issues/6243>,
  * I managed to write a context match on the body of the forall. *)

Ltac fold_not_under_forall :=
   repeat
     match goal with
     | H : forall n : ?T, @?x n |- _ =>
       match x with
       | fun n : T => ?b =>
         let not_n := fresh in
         let b''' :=
             constr:(
               fun n : T =>
                 match b with
                 | not_n =>
                   ltac:(let b' := (eval cbv delta [not_n] in not_n) in
                         match b' with
                         | context C[?P -> False] =>
                           let b'' := context C[~ P] in
                           exact b''
                         end)
                 end) in
         let tH' := eval cbn beta in (forall n : T, b''' n) in
             let tH := type of H in
             change tH with tH' in H
       end
     end.

Goal (forall n : nat, ((n >= 0) -> False) -> False) -> True.
   intro.
   (* H : forall n : nat, (n >= 0 -> False) -> False *)
   fold_not_under_forall.
   (* H : forall n : nat, ~ ~ n >= 0 *)
Abort.

(* It works, but it's the ugliest Ltac I've ever written.
  * Hopefully it can be improved? *)