des* doesn't terminate terminate if it deconstructs a section variable

[anlun]

In the following code, desc terminates in the proof of ff but doesn't in the proof of ff'.

From hahn Require Import Hahn.

Theorem ff (HH : << AA : True >> /\ << BB : True >>) : False.
Proof.
  desc.
Admitted.

Section aa.
  Variable HH : << AA : True >> /\ << BB : True >>.

  Theorem ff' : False.
  Proof.
    desc.
  Admitted.
End aa.

The same problem is presented if we replace desc with its part:

repeat match goal with
  | H : ?p /\ ?q |- _ =>
    let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
    let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
    destruct H as [x' y'];
    match p with | NW _ => red in x' | _ => idtac end;
    match q with | NW _ => red in y' | _ => idtac end
end.

That is, the problem appears since destruct HH doesn't remove HH from hypotheses if HH is a section variable.

Replacing destruct H as [x' y'] with destruct H as [x' y']; clear H in the tactic solves the problem. I propose to update the des* family of tactics in that way.

[vafeiadis]

Thanks. I think the right Ltac sequence is:

repeat match goal with | H : ?p /\ ?q |- => let x' := match p with | NW (fun z => ) => fresh z | => H end in let y' := match q with | NW (fun z => ) => fresh z | => fresh H end in generalize H; clear H; intros [x' y']; match p with | NW => red in x' | => idtac end ; match q with | NW => red in y' | _ => idtac end end.

[anlun]

@vafeiadis should I make a pull request w/ the changes?

[vafeiadis]

Yes. Could also please check that promise2 compiles with the changes?

On 16. Nov 2019, at 10:22, Anton Podkopaev notifications@github.com wrote:

@vafeiadis should I make a pull request w/ the changes?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

[anlun]

@vafeiadis promise2 doesn't use hahn, but I'll check that our projects (imm, weakestmoToImm, promise2ToImm) compile

[anlun]

BTW, there is the same problem w/ Variable HH : exists b, << AA : b = True >>.

[vafeiadis]

Yes, also disjuction, etc. In all cases, you'll have to replace destruct with generalize; clear; intros

On 16. Nov 2019, at 10:33, Anton Podkopaev notifications@github.com wrote:

BTW, there is the same problem w/ Variable HH : exists b, << AA : b = True >>.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

[anlun]

@vafeiadis I tried to fix the issue in #13, but for a strange reason it breaks compilation on l. 216 in HahnTotalList.v. It's super strange because after the l. 215 the goal and hypotheses are exactly the same. I even checked them w/ Set Printing All.

[vafeiadis]

Fixed by a0cbf4c77971027dc170a7c961ef8f8773741353