PolCert/polygen/PolyTest.v at extractor · Hughshine/PolCert · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
(* *****************************************************************)
(*                                                                 *)
(*               Verified polyhedral AST generation                *)
(*                                                                 *)
(*                 Nathanaël Courant, Inria Paris                  *)
(*                                                                 *)
(*  Copyright Inria. All rights reserved. This file is distributed *)
(*  under the terms of the GNU Lesser General Public License as    *)
(*  published by the Free Software Foundation, either version 2.1  *)
(*  of the License, or (at your option) any later version.         *)
(*                                                                 *)
(* *****************************************************************)

Require Import ZArith.
Require Import Bool.
Require Import List.
Require Import Psatz.

Require Import Misc.
Require Import Linalg.
Require Import VplInterface.
Require Import Projection.
Require Import ImpureAlarmConfig.

Open Scope Z_scope.

Definition isBottom pol :=
  BIND p <- lift (ExactCs.fromCs_unchecked (poly_to_Cs pol)) -; lift (CstrDomain.isBottom p).

Lemma isBottom_correct :
  forall pol t, 0 < t -> If isBottom pol THEN forall p, in_poly p (expand_poly t pol) = false.
Proof.
  intros pol t Ht b Hbot.
  destruct b; simpl; [|auto]. intros p.
  unfold isBottom in Hbot.
  apply mayReturn_bind in Hbot; destruct Hbot as [p1 [Hp1 Hbot]].
  apply mayReturn_lift in Hp1; apply mayReturn_lift in Hbot.
  apply CstrDomain.isBottom_correct in Hbot; simpl in Hbot.
  apply ExactCs.fromCs_unchecked_correct in Hp1.
  apply not_true_is_false; intros Hin.
  rewrite <- poly_to_Cs_correct_Q in Hin by auto.
  eauto.
Qed.

Lemma isBottom_correct_1 :
  forall pol, If isBottom pol THEN forall p, in_poly p pol = false.
Proof.
  intros pol. generalize (isBottom_correct pol 1).
  rewrite expand_poly_1. intros H; apply H; lia.
Qed.

Definition isIncl pol1 pol2 :=
  BIND p1 <- lift (ExactCs.fromCs_unchecked (poly_to_Cs pol1)) -;
  BIND p2 <- lift (ExactCs.fromCs (poly_to_Cs pol2)) -;
  match p2 with Some p2 => lift (CstrDomain.isIncl p1 p2) | None => pure false end.

Lemma isIncl_correct :
  forall pol1 pol2 t, 0 < t -> If isIncl pol1 pol2 THEN forall p, in_poly p (expand_poly t pol1) = true -> in_poly p (expand_poly t pol2) = true.
Proof.
  intros pol1 pol2 t Ht b Hincl.
  destruct b; simpl; [|auto]. intros p Hin.
  unfold isIncl in Hincl.
  bind_imp_destruct Hincl p1 Hp1; bind_imp_destruct Hincl p2 Hp2.
  destruct p2 as [p2|]; [|apply mayReturn_pure in Hincl; congruence].
  apply mayReturn_lift in Hp1; apply mayReturn_lift in Hp2; apply mayReturn_lift in Hincl.
  apply CstrDomain.isIncl_correct in Hincl; simpl in Hincl.
  apply ExactCs.fromCs_unchecked_correct in Hp1.
  eapply ExactCs.fromCs_correct in Hp2.
  rewrite <- poly_to_Cs_correct_Q in Hin by auto.
  apply Hp1, Hincl in Hin. rewrite Hp2 in Hin.
  rewrite poly_to_Cs_correct_Q in Hin by auto.
  auto.
Qed.

Lemma isIncl_correct_1 :
  forall pol1 pol2, If isIncl pol1 pol2 THEN forall p, in_poly p pol1 = true -> in_poly p pol2 = true.
Proof.
  intros pol1 pol2. generalize (isIncl_correct pol1 pol2 1).
  rewrite !expand_poly_1. intros H; apply H; lia.
Qed.


Definition canPrecede n pol1 pol2 :=
  forall p1 x, in_poly p1 pol1 = true ->
    in_poly (assign n x p1) pol2 = true -> nth n p1 0 < x.

Definition check_canPrecede n (pol1 pol2 proj1 : polyhedron) :=
  let g1 := filter (fun c => 0 <? nth n (fst c) 0) pol1 in
  isBottom (pol2 ++ proj1 ++ g1).

Lemma check_canPrecede_correct :
  forall n pol1 pol2 proj1,
    isExactProjection n pol1 proj1 ->
    If check_canPrecede n pol1 pol2 proj1 THEN canPrecede n pol1 pol2.
Proof.
  intros n pol1 pol2 proj1 Hproj1 b Hprec.
  destruct b; simpl; [|auto].
  intros p1 x Hp1 Hpx.
  unfold check_canPrecede in Hprec. apply isBottom_correct_1 in Hprec; simpl in Hprec.
  specialize (Hprec (assign n x p1)). rewrite !in_poly_app in Hprec. reflect.
  rewrite Hpx in Hprec.
  apply isExactProjection_weaken1 in Hproj1. eapply isExactProjection_assign_1 in Hproj1; [|exact Hp1].
  rewrite Hproj1 in Hprec.
  destruct Hprec as [? | [? | Hprec]]; try congruence.
  assert (Hin : in_poly p1 (filter (fun c => 0 <? nth n (fst c) 0) pol1) = true).
  - unfold in_poly in *; rewrite forallb_forall in *.
    intros c. rewrite filter_In. intros; apply Hp1; tauto.
  - rewrite <- Z.nle_gt. intros Hle.
    eapply eq_true_false_abs; [|exact Hprec].
    unfold in_poly in *; rewrite forallb_forall in *.
    intros c. rewrite filter_In. intros Hc.
    specialize (Hin c). rewrite filter_In in Hin. specialize (Hin Hc).
    destruct Hc as [Hcin Hc].
    unfold satisfies_constraint in *. reflect. rewrite dot_product_assign_left.
    nia.
Qed.