The Coq mailing list

[ikdc <ikdc AT mit.edu>]

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