@@ -449,13 +449,17 @@ Ltac try_prove_it_now :=
449
449
where B and D are easily provable, one wants to leave the
450
450
goal A/\C.
451
451
*)
452
+
453
+ Definition conjuncts_marker (P: Prop) : Prop := P.
454
+ (* The purpose of this conjuncts marker is to try to address VST issue #745 *)
455
+
452
456
Lemma try_conjuncts_lem2: forall A B : Prop,
453
457
B -> A -> (A /\ B).
454
458
Proof . tauto. Qed .
455
459
456
460
Lemma try_conjuncts_lem: forall A B A' B' : Prop,
457
- (A -> A') -> (B -> B') -> (A /\ B -> A' /\ B').
458
- Proof . tauto. Qed .
461
+ (conjuncts_marker A -> A') -> (conjuncts_marker B -> B') -> (( A /\ B) -> A' /\ B').
462
+ Proof . unfold conjuncts_marker; tauto. Qed .
459
463
460
464
Lemma try_conjuncts_start: forall A B: Prop,
461
465
(A -> B) -> (A -> B).
@@ -468,22 +472,23 @@ Ltac try_conjuncts_solver :=
468
472
end .
469
473
470
474
Ltac try_conjuncts :=
471
- first [ simple eapply conj;
475
+ first [ simple apply conj;
472
476
[try_conjuncts_solver | try_conjuncts ]
473
477
| simple eapply try_conjuncts_lem2;
474
- [try_conjuncts_solver | match goal with H:_ |- _ => apply H end ]
478
+ [try_conjuncts_solver
479
+ | match goal with H: conjuncts_marker _ |- _ => red in H; apply H end ]
475
480
| simple eapply try_conjuncts_lem;
476
481
[intro; try_conjuncts | intro; try_conjuncts
477
- |match goal with H:_ |- _ => apply H end ]
478
- | match goal with H:_ |- _ => instantiate (1:=True) in H;
482
+ |match goal with H: conjuncts_marker _ |- _ => red in H; apply H end ]
483
+ | match goal with H: conjuncts_marker _ |- _ => instantiate (1:=True) in H;
479
484
try_conjuncts_solver
480
485
end
481
- | match goal with H:_ |- _ => apply H end
486
+ | match goal with H: conjuncts_marker _ |- _ => red in H; apply H end
482
487
].
483
488
484
489
Lemma try_conjuncts_prop_and:
485
490
forall {A}{NA: NatDed A} (S: A) (P P': Prop) Q,
486
- (P' -> P) ->
491
+ (conjuncts_marker P' -> P) ->
487
492
(S |-- !! P' && Q) ->
488
493
S |-- !! P && Q.
489
494
Proof . intros.
495
500
496
501
Lemma try_conjuncts_prop:
497
502
forall {A}{NA: NatDed A} (S: A) (P P': Prop),
498
- (P' -> P) ->
503
+ (conjuncts_marker P' -> P) ->
499
504
(S |-- !! P') ->
500
505
S |-- !! P .
501
506
Proof . intros.
535
540
Ltac clean_up_stackframe := idtac.
536
541
537
542
Lemma my_auto_lem:
538
- forall (P Q: Prop), (P -> Q) -> (P -> Q).
543
+ forall (P Q: Prop), (conjuncts_marker P -> Q) -> (P -> Q).
539
544
Proof . auto. Qed .
540
545
541
546
Ltac my_auto_iter H :=
@@ -545,7 +550,7 @@ Ltac my_auto_iter H :=
545
550
[let H1 := fresh in intro H1; my_auto_iter H1
546
551
|let H1 := fresh in intro H1; my_auto_iter H1
547
552
| apply H ]
548
- | apply H
553
+ | red in H (* remove conjuncts_marker *) ; apply H
549
554
].
550
555
551
556
Ltac all_True := solve [repeat simple apply conj; simple apply Coq.Init.Logic.I].
@@ -557,7 +562,7 @@ Ltac my_auto_reiter :=
557
562
[intro; my_auto_reiter
558
563
|intro; my_auto_reiter
559
564
|eassumption]
560
- |eassumption ].
565
+ |lazymatch goal with H: conjuncts_marker _ |- _ => red in H; apply H end ].
561
566
562
567
Ltac my_auto :=
563
568
repeat match goal with |- ?P -> _ => match type of P with Prop => intro end end ;
0 commit comments