The Coq mailing list

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

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? *)