rocq/theories/Sites.v
Where a name is defined, and what definitions_dominate/3 says of its uses (formal.md, Campaign 3; rocq.md, Where a name is defined).
ir.pl reads a function's definitions twice: as the list of definitions single_definitions/3 filters (Validate.v's all_defs), and as the definition sites block_sites//1 records for the strict SSA check (temp_sites). The run-level invariant needs both at once: the relation a single definition states holds wherever its site dominates the running point. This file joins the two through one list of every definition with its site, def_positions.
Decisions
| Decision | Why |
|---|---|
positions are sites, the validator's own | site_dominates/4 is then the order the invariant uses, with no second notion of position |
def_positions is a new list, proved equal to all_defs without sites | Validate.v, the transcription the gates compare, stays as it is |
| a single definition is unique by counting | single_definitions/3 keeps a name defined once in the list; two positions would be two entries |
From Stdlib Require Import String ZArith List Bool Lia
From Nanofil Require Import Term Maps Syntax Cfg Validate Dominance
Import ListNotations
Open Scope Z_scope
Every definition with its site
The definitions the instructions is make in the block labelled l, the first at index j: each name an instruction defines, with its site at the instruction's index and the instruction as its definition.
match is with
[ ]
⇒
[ ]
Every definition of the function f with its site: its parameters at SParam, then each block's block_positions. The one list that joins the two ways the validator reads definitions.
mapλp ⇒ sndp, SParam, DParam fn_paramsf ++ flat_mapblock_positions fn_blocksf
Forgets the site of a definition, leaving the pair of a name and its definition that all_defs lists.
Without their sites, the definitions inst_positions lists for some instructions are those all_defs lists for them, whatever the label and first index.
∀ l j is
flat_mapλi ⇒ mapλdk ⇒ fstdk, DInsti inst_temp_defsi is = mapdrop_site inst_positionsl j is
Explore proof 6 tactics
Initial goal
⊢
∀l : name j : Z is : listinst, flat_mapλi : inst ⇒ mapλdk : name × class ⇒ fstdk, DInsti inst_temp_defsi is = mapdrop_site inst_positionsl j is
intros l j is
⊢
flat_mapλi : inst ⇒ mapλdk : name × class ⇒ fstdk, DInsti inst_temp_defsi is = mapdrop_site inst_positionsl j is
revert j
⊢
∀j : Z, flat_mapλi : inst ⇒ mapλdk : name × class ⇒ fstdk, DInsti inst_temp_defsi is = mapdrop_site inst_positionsl j is
induction is as | i rest IH ; intros j ; reflexivity |
l :
i :
rest :
listinst
IH :
∀j : Z, flat_mapλi : inst ⇒ mapλdk : name × class ⇒ fstdk, DInsti inst_temp_defsi rest = mapdrop_site inst_positionsl j rest
j :
Z
⊢
flat_mapλi0 : inst ⇒ mapλdk : name × class ⇒ fstdk, DInsti0 inst_temp_defsi0 i :: rest = mapdrop_site inst_positionsl j i :: rest
simpl
l :
i :
rest :
listinst
IH :
∀j : Z, flat_mapλi : inst ⇒ mapλdk : name × class ⇒ fstdk, DInsti inst_temp_defsi rest = mapdrop_site inst_positionsl j rest
j :
Z
⊢
mapλdk : name × class ⇒ fstdk, DInsti inst_temp_defsi ++ flat_mapλi0 : inst ⇒ mapλdk : name × class ⇒ fstdk, DInsti0 inst_temp_defsi0 rest = mapdrop_site mapλdk : name × class ⇒ fstdk, SAtl j, DInsti inst_temp_defsi ++ inst_positionsl j + 1 rest
rewrite map_app , IHj + 1 , map_map
l :
i :
rest :
listinst
IH :
∀j : Z, flat_mapλi : inst ⇒ mapλdk : name × class ⇒ fstdk, DInsti inst_temp_defsi rest = mapdrop_site inst_positionsl j rest
j :
Z
⊢
mapλdk : name × class ⇒ fstdk, DInsti inst_temp_defsi ++ mapdrop_site inst_positionsl j + 1 rest = mapλx : name × class ⇒ drop_sitefstx, SAtl j, DInsti inst_temp_defsi ++ mapdrop_site inst_positionsl j + 1 rest
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros l j is
revert j
induction is as | i rest IH ; intros j ; reflexivity |
simpl
rewrite map_app , IHj + 1 , map_map
reflexivity
all_defs, Validate.v's list of every definition that single_definitions/3 filters, is def_positions without the sites.
∀ f
all_defsf = mapdrop_site def_positionsf
Explore proof 14 tactics
Initial goal
⊢
∀f : func, all_defsf = mapdrop_site def_positionsf
intros f
f :
⊢
all_defsf = mapdrop_site def_positionsf
unfold all_defs , def_positions
f :
⊢
++
=
rewrite map_app , map_map
f :
⊢
++
=
f_equal
induction fn_blocksf as | b bs IH ; reflexivity |
simpl
⊢
rewrite map_app , <- IH
⊢
++
++
=
f_equal
unfold block_positions
rewrite map_app , map_map , <- inst_positions_defsb_labelb 0
f_equal
apply map_ext
intros d k pairs
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros f
unfold all_defs , def_positions
rewrite map_app , map_map
f_equal
induction fn_blocksf as | b bs IH ; reflexivity |
simpl
rewrite map_app , <- IH
f_equal
unfold block_positions
rewrite map_app , map_map , <- inst_positions_defsb_labelb 0
f_equal
apply map_ext
intros d k pairs
reflexivity
The sites temp_sites records
A map m from each name to sites is sound for the function f when every site it records for a name n is a position of def_positions that defines n.
∀n ss s, nm_findn m = Somess → Ins ss → ∃d, Inn, s, d def_positionsf
Records the site s for the name n in front of n's list in m, as temp_sites does.
Recording a site s for n keeps the map sound when s is the position of some definition of n in f.
Explore proof 10 tactics
Initial goal
intros f m n s d Hm Hd k ss s′ E Hin
unfold add_site in E
rewrite nm_find_add in E
destruct name_eqbk n eqn: Ek
2 openf :
n :
s :
d :
Hm :
sites_okf m
Hd :
Inn, s, d def_positionsf
k :
ss :
listsite
s′ :
Ek :
name_eqbk n = true
E :
Hin :
Ins′ ss
⊢
∃d0 : def, Ink, s′, d0 def_positionsf
–apply name_eqb_true in Ek
2 open⊢
∃d0 : def, Ink, s′, d0 def_positionsf
subst k
2 open⊢
∃d0 : def, Inn, s′, d0 def_positionsf
injection E as ←
2 open⊢
∃d0 : def, Inn, s′, d0 def_positionsf
destruct Hin as ← | Hin ; eauto |
2 open⊢
∃d0 : def, Inn, s′, d0 def_positionsf
destruct nm_findn m as ss0 | eqn: E0 ; exact Hm_ _ _ E0 Hin | destruct Hin
–exact Hm_ _ _ E Hin
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros f m n s d Hm Hd k ss s′ E Hin
unfold add_site in E
rewrite nm_find_add in E
destruct name_eqbk n eqn: Ek
–apply name_eqb_true in Ek
subst k
injection E as ←
destruct Hin as ← | Hin ; eauto |
destruct nm_findn m as ss0 | eqn: E0 ; exact Hm_ _ _ E0 Hin | destruct Hin
–exact Hm_ _ _ E Hin
Recording a list of sites, the name and site g gives each element of xs, keeps the map sound when each is the position of some definition in f.
Explore proof 6 tactics
Initial goal
intros A f g xs
induction xs as | x xs IH ; intros m Hm Hx ; exact Hm |
A :
Type
f :
x :
A
xs :
listA
IH :
Hm :
sites_okf m
Hx :
∀x0 : A, Inx0 x :: xs → ∃d : def, Infstgx0, sndgx0, d def_positionsf
simpl
A :
Type
f :
x :
A
xs :
listA
IH :
Hm :
sites_okf m
Hx :
∀x0 : A, Inx0 x :: xs → ∃d : def, Infstgx0, sndgx0, d def_positionsf
apply IH ; | intros y Hy ; apply Hx ; right ; exact Hy
A :
Type
f :
x :
A
xs :
listA
IH :
Hm :
sites_okf m
Hx :
∀x0 : A, Inx0 x :: xs → ∃d : def, Infstgx0, sndgx0, d def_positionsf
destruct Hxx or_introleq_refl as d Hd
A :
Type
f :
x :
A
xs :
listA
IH :
Hm :
sites_okf m
Hx :
∀x0 : A, Inx0 x :: xs → ∃d : def, Infstgx0, sndgx0, d def_positionsf
d :
Hd :
Infstgx, sndgx, d def_positionsf
exact add_site_ok_ _ _ _ _ Hm Hd
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros A f g xs
induction xs as | x xs IH ; intros m Hm Hx ; exact Hm |
simpl
apply IH ; | intros y Hy ; apply Hx ; right ; exact Hy
destruct Hxx or_introleq_refl as d Hd
exact add_site_ok_ _ _ _ _ Hm Hd
The fold temp_sites makes over the instructions is of the block labelled l, from index j, keeps the map sound when every position inst_positions lists for them is one of f's.
∀ f l is j m
sites_okf m
∀t, Int inst_positionsl j is → Int def_positionsf
Explore proof 14 tactics
Initial goal
⊢
intros f l is
induction is as | i rest IH ; intros j m Hm Hp ; exact Hm |
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
simpl
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
apply IH ; | intros t Ht ; apply Hp ; simpl ; apply in_or_app ; right ; exact Ht
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
apply fold_sites_ok_ f λdk ⇒ fstdk, SAtl j ; exact Hm |
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
⊢
∀x : name × class, Inx inst_temp_defsi → ∃d : def, Infstfstx, SAtl j, sndfstx, SAtl j, d def_positionsf
intros dk Hdk
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
Hdk :
Indk inst_temp_defsi
⊢
∃d : def, Infstfstdk, SAtl j, sndfstdk, SAtl j, d def_positionsf
exists DInsti
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
Hdk :
Indk inst_temp_defsi
⊢
Infstfstdk, SAtl j, sndfstdk, SAtl j, DInsti def_positionsf
apply Hp
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
Hdk :
Indk inst_temp_defsi
⊢
Infstfstdk, SAtl j, sndfstdk, SAtl j, DInsti inst_positionsl j i :: rest
simpl
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti inst_temp_defsi ++ inst_positionsl j + 1 rest
apply in_or_app
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti inst_temp_defsi ∨ Infstdk, SAtl j, DInsti inst_positionsl j + 1 rest
left
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
Hdk :
Indk inst_temp_defsi
apply in_map_iff
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
Hdk :
Indk inst_temp_defsi
exists dk
f :
l :
i :
rest :
listinst
IH :
j :
Z
Hm :
sites_okf m
Hp :
∀t : name × site × def, Int inst_positionsl j i :: rest → Int def_positionsf
Hdk :
Indk inst_temp_defsi
⊢
fstdk, SAtl j, DInsti = fstdk, SAtl j, DInsti ∧ Indk inst_temp_defsi
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros f l is
induction is as | i rest IH ; intros j m Hm Hp ; exact Hm |
simpl
apply IH ; | intros t Ht ; apply Hp ; simpl ; apply in_or_app ; right ; exact Ht
apply fold_sites_ok_ f λdk ⇒ fstdk, SAtl j ; exact Hm |
intros dk Hdk
exists DInsti
apply Hp
simpl
apply in_or_app
left
apply in_map_iff
exists dk
auto
Every site block_sites//1 records for a name n in temp_sites, the sites the validator's strict SSA check reads, is a position of def_positions that defines n.
Proof 46 steps Qed
intros f
unfold temp_sites
fold add_site
{apply fold_sites_ok_ f λp ⇒ sndp, SParam
assert Hb : ∀bs m, sites_okf m → ∀b, Inb bs → Inb fn_blocksf → sites_okf fold_leftλm b ⇒ let m1 ≔ fold_leftλm ph ⇒ match ph with Phid _ _ ⇒ add_sitem d SAtb_labelb −1 end b_phisb m in fstfold_leftλacc : nmaplistsite × Z ins ⇒ let m, j ≔ acc in fold_leftλm dk ⇒ add_sitem fstdk SAtb_labelb j inst_temp_defsins m, j + 1 b_instsb m1, 0 bs m
{intros bs
induction bs as | b bs IH ; intros m Hm Hin ; exact Hm |
simpl
apply IH ; | intros b′ Hb′ ; apply Hin ; right ; exact Hb'
assert Hpos : ∀t, Int block_positionsb → Int def_positionsf
{intros t Ht
unfold def_positions
apply in_or_app
right
apply in_flat_map
exists b
split ; apply Hin ; left ; reflexivity | exact Ht
apply inst_fold_sites_ok ; | intros t Ht ; apply Hpos ; unfold block_positions ; apply in_or_app ; right ; exact Ht
assert Hph : ∀xs m0, sites_okf m0 → ∀ph, Inph xs → Inph b_phisb → sites_okf fold_leftλm ph ⇒ match ph with Phid _ _ ⇒ add_sitem d SAtb_labelb −1 end xs m0
{intros xs
induction xs as | d k pairs xs IHx ; intros m0 Hm0 Hx ; exact Hm0 |
simpl
apply IHx ; | intros ph Hph ; apply Hx ; right ; exact Hph
apply add_site_ok_ _ _ _ DPhiPhid k pairs Hm0
apply Hpos
unfold block_positions
apply in_or_app
left
apply in_map_iff
split ; reflexivity | apply Hx ; left ; reflexivity
exact Hph_ _ Hm λph H ⇒ H
intros n ss s E Hin
exact Hb_ _ Hp λb H ⇒ H n ss s E Hin
A single definition has one position
Filtering a mapped list keeps as many elements as filtering the list by the test composed with the map.
lengthfilterp mapg l = lengthfilterλx ⇒ pgx l
Explore proof 3 tactics
Initial goal
intros A B p g l
A :
Type
B :
Type
p :
B → bool
g :
A → B
l :
listA
⊢
Datatypes.lengthfilterp mapg l = Datatypes.lengthfilterλx : A ⇒ pgx l
induction l as | x l IH ; simpl ; reflexivity |
A :
Type
B :
Type
p :
B → bool
g :
A → B
x :
A
l :
listA
IH :
Datatypes.lengthfilterp mapg l = Datatypes.lengthfilterλx : A ⇒ pgx l
⊢
Datatypes.length
pgx
→
gx :: filterp mapg l
else
filterp mapg l
=
Datatypes.length
pgx
→
x :: filterλx0 : A ⇒ pgx0 l
else
filterλx0 : A ⇒ pgx0 l
destruct pgx ; simpl ; auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros A B p g l
induction l as | x l IH ; simpl ; reflexivity |
destruct pgx ; simpl ; auto
A name n that single_definitions/3 keeps, with its definition d, has exactly one position in def_positions, and that position holds d.
∀ f n d
lookupn single_definitionsf = Somed
∃s, Inn, s, d def_positionsf ∧ ∀s′ d′, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
Explore proof 32 tactics
Initial goal
⊢
∀f : func n : name d : def, lookupn single_definitionsf = Somed → ∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
intros f n d H
⊢
∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
destruct lookup_some_in_ _ _ _ H as n′ & En & Hin
f :
n :
d :
H :
lookupn single_definitionsf = Somed
n′ :
En :
name_eqbn n′ = true
Hin :
Inn′, d single_definitionsf
⊢
∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
apply name_eqb_true in En
⊢
∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
subst n′
⊢
∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
unfold single_definitions in Hin
apply filter_In in Hin as Hall Hcount
⊢
∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
apply Nat.eqb_eq in Hcount
⊢
∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
simpl in Hcount
⊢
∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
rewrite all_defs_positions in Hall , Hcount
f :
n :
d :
H :
lookupn single_definitionsf = Somed
Hall :
Inn, d mapdrop_site def_positionsf
Hcount :
Datatypes.lengthfilterλd′ : name × def ⇒ name_eqbn fstd′ mapdrop_site def_positionsf = 1%nat
⊢
∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
rewrite filter_map_length in Hcount
⊢
∃s : site, Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
apply in_map_iff in Hall as n0 s d0 & Ed & Hs
f :
n :
d :
H :
lookupn single_definitionsf = Somed
n0 :
s :
d0 :
Ed :
drop_siten0, s, d0 = n, d
Hs :
Inn0, s, d0 def_positionsf
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
unfold drop_site in Ed
f :
n :
d :
H :
lookupn single_definitionsf = Somed
n0 :
s :
d0 :
Ed :
fstfstn0, s, d0, sndn0, s, d0 = n, d
Hs :
Inn0, s, d0 def_positionsf
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
simpl in Ed
f :
n :
d :
H :
lookupn single_definitionsf = Somed
n0 :
s :
d0 :
Ed :
n0, d0 = n, d
Hs :
Inn0, s, d0 def_positionsf
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
injection Ed as → →
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
set L := filterλt ⇒ name_eqbn fstdrop_sitet def_positionsf in Hcount
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
assert HL : ∀s′ d′, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
2 openf :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
⊢
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
focused goal
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
{intros s′ d′ Hs′
2 openf :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
⊢
Inn, s′, d′ L
deferred goal
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
apply filter_In
2 openf :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
⊢
Inn, s′, d′ def_positionsf ∧ name_eqbn fstdrop_siten, s′, d′ = true
deferred goal
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
split ; exact Hs′ |
2 openf :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
deferred goal
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
apply name_eqb_true
2 openf :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
⊢
n = fstdrop_siten, s′, d′
deferred goal
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
reflexivity
deferred goal
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
⊢
∃s0 : site, Inn, s0, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s0 ∧ d′ = d
exists s
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
⊢
Inn, s, d def_positionsf ∧ ∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
split ; exact Hs |
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
⊢
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → s′ = s ∧ d′ = d
intros s′ d′ Hs′
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
⊢
s′ = s ∧ d′ = d
pose proof HL_ _ Hs as H1
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
H1 :
Inn, s, d L
⊢
s′ = s ∧ d′ = d
pose proof HL_ _ Hs′ as H2
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
Datatypes.lengthL = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
H1 :
Inn, s, d L
H2 :
Inn, s′, d′ L
⊢
s′ = s ∧ d′ = d
destruct L as | t | t′ L′ ; simpl in Hcount ; try discriminate Hcount
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
1%nat = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ t
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
H1 :
Inn, s, d t
H2 :
Inn, s′, d′ t
⊢
s′ = s ∧ d′ = d
destruct H1 as E1 |
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
1%nat = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ t
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
E1 :
t = n, s, d
H2 :
Inn, s′, d′ t
⊢
s′ = s ∧ d′ = d
destruct H2 as E2 |
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
1%nat = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ t
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
E1 :
t = n, s, d
E2 :
t = n, s′, d′
⊢
s′ = s ∧ d′ = d
rewrite E1 in E2
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
1%nat = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ t
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
E1 :
t = n, s, d
E2 :
n, s, d = n, s′, d′
⊢
s′ = s ∧ d′ = d
injection E2 as E3 E4
f :
n :
d :
H :
lookupn single_definitionsf = Somed
s :
Hs :
Inn, s, d def_positionsf
Hcount :
1%nat = 1%nat
HL :
∀s′ : site d′ : def, Inn, s′, d′ def_positionsf → Inn, s′, d′ t
s′ :
d′ :
Hs′ :
Inn, s′, d′ def_positionsf
E1 :
t = n, s, d
E3 :
s = s′
E4 :
d = d′
⊢
s′ = s ∧ d′ = d
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros f n d H
destruct lookup_some_in_ _ _ _ H as n′ & En & Hin
apply name_eqb_true in En
subst n′
unfold single_definitions in Hin
apply filter_In in Hin as Hall Hcount
apply Nat.eqb_eq in Hcount
simpl in Hcount
rewrite all_defs_positions in Hall , Hcount
rewrite filter_map_length in Hcount
apply in_map_iff in Hall as n0 s d0 & Ed & Hs
unfold drop_site in Ed
simpl in Ed
injection Ed as → →
set L := filterλt ⇒ name_eqbn fstdrop_sitet def_positionsf in Hcount
assert HL : ∀s′ d′, Inn, s′, d′ def_positionsf → Inn, s′, d′ L
exists s
split ; exact Hs |
intros s′ d′ Hs′
pose proof HL_ _ Hs as H1
pose proof HL_ _ Hs′ as H2
destruct L as | t | t′ L′ ; simpl in Hcount ; try discriminate Hcount
destruct H1 as E1 |
destruct H2 as E2 |
rewrite E1 in E2
injection E2 as E3 E4
auto
A use is dominated by its single definition
In a function f whose definitions dominate their uses (definitions_dominate), a name o with a single definition d that the instruction at place k of a reachable block b uses is defined at a site that dominates that place (site_dominates).
∀ f doms b k ins o d
definitions_dominatef doms = true
Inb fn_blocksf
is_reachabledoms b_labelb = true
nth_errorb_instsb k = Someins
Ino inst_usesins
lookupo single_definitionsf = Somed
∃s, Ino, s, d def_positionsf ∧ site_dominatesdoms b_labelb Z.of_natk s = true
Proof 30 steps Qed
intros f doms b k ins o d H Hb Hr Hk Hu Ho
unfold definitions_dominate in H
rewrite forallb_forall in H
specialize Hb Hb
rewrite Hr in H
simpl in H
apply andb_true_iff in H as Hi _
assert Hdu : dominated_usetemp_sitesf doms b_labelb Z.of_natk o = true
{match type of Hi withb_instsb 0 = true⇒assert G : ∀is i k ins, Fis i = true → nth_erroris k = Someins → Ino inst_usesins → dominated_usetemp_sitesf doms b_labelb i + Z.of_natk o = trueend
{intros is
induction is as | ins0 rest IH ; intros i k0 ins1 Hf Hn Hin ; destruct k0 ; discriminate Hn |
cbn in Hf
apply andb_true_iff in Hf as Hf1 Hf2
destruct k0 as | k0 ; simpl in Hn
–rewrite Nat2Z.inj_succ
replace i + Z.succZ.of_natk0 with i + 1 + Z.of_natk0 by lia
exact IH_ _ _ Hf2 Hn Hin
exact G_ _ _ _ Hi Hk Hu
unfold dominated_use in Hdu
destruct nm_findo temp_sitesf as ss | eqn: Es ; | discriminate Hdu
apply existsb_exists in Hdu as s & Hin & Hd
destruct temp_sites_sound_ _ _ _ Es Hin as d′ Hd′
destruct once_position_ _ _ Ho as s0 & Hs0 & Huniq
destruct Huniq_ _ Hd' as → →
exists s0
auto
Positions and instructions
name_eqb is symmetric.
Explore proof 10 tactics
Initial goal
intros a b
destruct name_eqba b eqn: E ; symmetry
2 open–apply name_eqb_true in E
2 opensubst
2 openapply name_eqb_true
2 openb :
⊢
b = b
reflexivity
–apply name_eqb_false
intros →
apply name_eqb_false in E
a :
E :
a ≠ a
⊢
False
exact Eeq_refl
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros a b
destruct name_eqba b eqn: E ; symmetry
A position that inst_positions lists for the instructions is of the block labelled l, from index j, is that of some instruction i at place k of is, at index j + k, and names a temporary i defines.
∀ l j is n s d
Inn, s, d inst_positionsl j is
∃k i, nth_erroris k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
Explore proof 18 tactics
Initial goal
⊢
∀l : name j : Z is : listinst n : name s : site d : def, Inn, s, d inst_positionsl j is → ∃k : nat i : inst, nth_erroris k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
intros l j is
⊢
∀n : name s : site d : def, Inn, s, d inst_positionsl j is → ∃k : nat i : inst, nth_erroris k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
revert j
⊢
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j is → ∃k : nat i : inst, nth_erroris k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
induction is as | i rest IH ; intros j n s d H ; destruct H |
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j i :: rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
simpl in H
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d mapλdk : name × class ⇒ fstdk, SAtl j, DInsti inst_temp_defsi ++ inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
apply in_app_or in H as H | H
2 openl :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d mapλdk : name × class ⇒ fstdk, SAtl j, DInsti inst_temp_defsi
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
focused goal
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
–apply in_map_iff in H as dk & E & Hdk
2 openl :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
Hdk :
Indk inst_temp_defsi
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
deferred goal
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
injection E as ← ← ←
2 openl :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
Hdk :
Indk inst_temp_defsi
deferred goal
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
exists O, i
2 openl :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
Hdk :
Indk inst_temp_defsi
⊢
nth_errori :: rest 0 = Somei ∧ SAtl j = SAtl j + Z.of_nat0 ∧ DInsti = DInsti ∧ Infstdk mapfst inst_temp_defsi
deferred goal
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
split ; reflexivity |
2 openl :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
Hdk :
Indk inst_temp_defsi
⊢
SAtl j = SAtl j + Z.of_nat0 ∧ DInsti = DInsti ∧ Infstdk mapfst inst_temp_defsi
deferred goal
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
split ; replace j + Z.of_nat0 with j by lia ; reflexivity |
2 openl :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
Hdk :
Indk inst_temp_defsi
⊢
DInsti = DInsti ∧ Infstdk mapfst inst_temp_defsi
deferred goal
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
split ; reflexivity |
2 openl :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
Hdk :
Indk inst_temp_defsi
⊢
Infstdk mapfst inst_temp_defsi
deferred goal
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
apply in_map
2 openl :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
Hdk :
Indk inst_temp_defsi
⊢
Indk inst_temp_defsi
deferred goal
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
exact Hdk
deferred goal
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
s :
d :
H :
Inn, s, d inst_positionsl j + 1 rest
⊢
∃k : nat i0 : inst, nth_errori :: rest k = Somei0 ∧ s = SAtl j + Z.of_natk ∧ d = DInsti0 ∧ Inn mapfst inst_temp_defsi0
–destruct IH_ _ _ _ H as k & i′ & Hk & → & → & Hn
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
k :
nat
i′ :
H :
Inn, SAtl j + 1 + Z.of_natk, DInsti′ inst_positionsl j + 1 rest
Hk :
nth_errorrest k = Somei′
Hn :
Inn mapfst inst_temp_defsi′
exists Sk, i′
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
k :
nat
i′ :
H :
Inn, SAtl j + 1 + Z.of_natk, DInsti′ inst_positionsl j + 1 rest
Hk :
nth_errorrest k = Somei′
Hn :
Inn mapfst inst_temp_defsi′
⊢
nth_errori :: rest Sk = Somei′ ∧ SAtl j + 1 + Z.of_natk = SAtl j + Z.of_natSk ∧ DInsti′ = DInsti′ ∧ Inn mapfst inst_temp_defsi′
split ; exact Hk |
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
k :
nat
i′ :
H :
Inn, SAtl j + 1 + Z.of_natk, DInsti′ inst_positionsl j + 1 rest
Hk :
nth_errorrest k = Somei′
Hn :
Inn mapfst inst_temp_defsi′
⊢
SAtl j + 1 + Z.of_natk = SAtl j + Z.of_natSk ∧ DInsti′ = DInsti′ ∧ Inn mapfst inst_temp_defsi′
split ; replace j + Z.of_natSk with j + 1 + Z.of_natk by lia ; reflexivity |
l :
i :
rest :
listinst
IH :
∀j : Z n : name s : site d : def, Inn, s, d inst_positionsl j rest → ∃k : nat i : inst, nth_errorrest k = Somei ∧ s = SAtl j + Z.of_natk ∧ d = DInsti ∧ Inn mapfst inst_temp_defsi
j :
Z
n :
k :
nat
i′ :
H :
Inn, SAtl j + 1 + Z.of_natk, DInsti′ inst_positionsl j + 1 rest
Hk :
nth_errorrest k = Somei′
Hn :
Inn mapfst inst_temp_defsi′
⊢
DInsti′ = DInsti′ ∧ Inn mapfst inst_temp_defsi′
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros l j is
revert j
induction is as | i rest IH ; intros j n s d H ; destruct H |
simpl in H
apply in_app_or in H as H | H
–apply in_map_iff in H as dk & E & Hdk
injection E as ← ← ←
exists O, i
split ; reflexivity |
split ; replace j + Z.of_nat0 with j by lia ; reflexivity |
split ; reflexivity |
apply in_map
exact Hdk
–destruct IH_ _ _ _ H as k & i′ & Hk & → & → & Hn
exists Sk, i′
split ; exact Hk |
split ; replace j + Z.of_natSk with j + 1 + Z.of_natk by lia ; reflexivity |
auto
Conversely, inst_positions lists each temporary dk that the instruction i at place k of is defines, at index j + k.
∀ l j is k i dk
nth_erroris k = Somei
Indk inst_temp_defsi
Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j is
Explore proof 16 tactics
Initial goal
⊢
∀l : name j : Z is : listinst k : nat i : inst dk : name × class, nth_erroris k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j is
intros l j is
⊢
∀k : nat i : inst dk : name × class, nth_erroris k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j is
revert j
⊢
∀j : Z k : nat i : inst dk : name × class, nth_erroris k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j is
induction is as | i0 rest IH ; intros j k i dk Hk Hdk ; destruct k ; discriminate Hk |
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errori0 :: rest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j i0 :: rest
simpl
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errori0 :: rest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ++ inst_positionsl j + 1 rest
apply in_or_app
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errori0 :: rest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j + 1 rest
destruct k as | k ; simpl in Hk
2 openl :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
i :
Hk :
Somei0 = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_nat0, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_nat0, DInsti inst_positionsl j + 1 rest
focused goal
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natSk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_natSk, DInsti inst_positionsl j + 1 rest
–injection Hk as ←
2 openl :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
Hdk :
Indk inst_temp_defsi0
⊢
Infstdk, SAtl j + Z.of_nat0, DInsti0 mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_nat0, DInsti0 inst_positionsl j + 1 rest
deferred goal
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natSk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_natSk, DInsti inst_positionsl j + 1 rest
left
2 openl :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
Hdk :
Indk inst_temp_defsi0
deferred goal
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natSk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_natSk, DInsti inst_positionsl j + 1 rest
apply in_map_iff
2 openl :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
Hdk :
Indk inst_temp_defsi0
deferred goal
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natSk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_natSk, DInsti inst_positionsl j + 1 rest
exists dk
2 openl :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
Hdk :
Indk inst_temp_defsi0
⊢
fstdk, SAtl j, DInsti0 = fstdk, SAtl j + Z.of_nat0, DInsti0 ∧ Indk inst_temp_defsi0
deferred goal
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natSk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_natSk, DInsti inst_positionsl j + 1 rest
split ; | exact Hdk
2 openl :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
Hdk :
Indk inst_temp_defsi0
deferred goal
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natSk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_natSk, DInsti inst_positionsl j + 1 rest
replace j + Z.of_nat0 with j by lia
2 openl :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
Hdk :
Indk inst_temp_defsi0
deferred goal
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natSk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_natSk, DInsti inst_positionsl j + 1 rest
reflexivity
deferred goal
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natSk, DInsti mapλdk0 : name × class ⇒ fstdk0, SAtl j, DInsti0 inst_temp_defsi0 ∨ Infstdk, SAtl j + Z.of_natSk, DInsti inst_positionsl j + 1 rest
–right
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + Z.of_natSk, DInsti inst_positionsl j + 1 rest
replace j + Z.of_natSk with j + 1 + Z.of_natk by lia
l :
i0 :
rest :
listinst
IH :
∀j : Z k : nat i : inst dk : name × class, nth_errorrest k = Somei → Indk inst_temp_defsi → Infstdk, SAtl j + Z.of_natk, DInsti inst_positionsl j rest
j :
Z
k :
nat
i :
Hk :
nth_errorrest k = Somei
Hdk :
Indk inst_temp_defsi
⊢
Infstdk, SAtl j + 1 + Z.of_natk, DInsti inst_positionsl j + 1 rest
exact IH_ _ _ _ Hk Hdk
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros l j is
revert j
induction is as | i0 rest IH ; intros j k i dk Hk Hdk ; destruct k ; discriminate Hk |
simpl
apply in_or_app
destruct k as | k ; simpl in Hk
–injection Hk as ←
left
apply in_map_iff
exists dk
split ; | exact Hdk
replace j + Z.of_nat0 with j by lia
reflexivity
–right
replace j + Z.of_natSk with j + 1 + Z.of_natk by lia
exact IH_ _ _ _ Hk Hdk
A position of f at index j of the block labelled d, holding the instruction i, comes from a block of f labelled d whose instruction at place j is i, and i defines the name.
∀ f n d j i
Inn, SAtd j, DInsti def_positionsf
∃b k, Inb fn_blocksf ∧ b_labelb = d ∧ nth_errorb_instsb k = Somei ∧ j = Z.of_natk ∧ Inn mapfst inst_temp_defsi
Explore proof 18 tactics
Initial goal
intros f n d j i H
unfold def_positions in H
apply in_app_or in H as H | H
2 openf :
n, d :
j :
Z
i :
⊢
∃b : block k : nat, Inb fn_blocksf ∧ b_labelb = d ∧ nth_errorb_instsb k = Somei ∧ j = Z.of_natk ∧ Inn mapfst inst_temp_defsi
–apply in_map_iff in H as p & E & _
2 open⊢
∃b : block k : nat, Inb fn_blocksf ∧ b_labelb = d ∧ nth_errorb_instsb k = Somei ∧ j = Z.of_natk ∧ Inn mapfst inst_temp_defsi
discriminate E
–apply in_flat_map in H as b & Hb & H
unfold block_positions in H
apply in_app_or in H as H | H
2 open+apply in_map_iff in H as d′ k′ pairs & E & _
2 opendiscriminate E
+destruct inst_positions_in_ _ _ _ _ _ H as k & i′ & Hk & Es & Ed & Hn
f :
n, d :
j :
Z
i :
b :
Hb :
Inb fn_blocksf
H :
Inn, SAtd j, DInsti inst_positionsb_labelb 0 b_instsb
k :
nat
i′ :
Hk :
nth_errorb_instsb k = Somei′
Hn :
Inn mapfst inst_temp_defsi′
⊢
∃b0 : block k0 : nat, Inb0 fn_blocksf ∧ b_labelb0 = d ∧ nth_errorb_instsb0 k0 = Somei ∧ j = Z.of_natk0 ∧ Inn mapfst inst_temp_defsi
injection Es as Ed′ Ej
f :
n, d :
j :
Z
i :
b :
Hb :
Inb fn_blocksf
H :
Inn, SAtd j, DInsti inst_positionsb_labelb 0 b_instsb
k :
nat
i′ :
Hk :
nth_errorb_instsb k = Somei′
Ed′ :
d = b_labelb
Ej :
j = Z.of_natk
Hn :
Inn mapfst inst_temp_defsi′
⊢
∃b0 : block k0 : nat, Inb0 fn_blocksf ∧ b_labelb0 = d ∧ nth_errorb_instsb0 k0 = Somei ∧ j = Z.of_natk0 ∧ Inn mapfst inst_temp_defsi
injection Ed as ←
f :
n, d :
j :
Z
i :
b :
Hb :
Inb fn_blocksf
H :
Inn, SAtd j, DInsti inst_positionsb_labelb 0 b_instsb
k :
nat
Hk :
nth_errorb_instsb k = Somei
Ed′ :
d = b_labelb
Ej :
j = Z.of_natk
Hn :
Inn mapfst inst_temp_defsi
⊢
∃b0 : block k0 : nat, Inb0 fn_blocksf ∧ b_labelb0 = d ∧ nth_errorb_instsb0 k0 = Somei ∧ j = Z.of_natk0 ∧ Inn mapfst inst_temp_defsi
exists b, k
f :
n, d :
j :
Z
i :
b :
Hb :
Inb fn_blocksf
H :
Inn, SAtd j, DInsti inst_positionsb_labelb 0 b_instsb
k :
nat
Hk :
nth_errorb_instsb k = Somei
Ed′ :
d = b_labelb
Ej :
j = Z.of_natk
Hn :
Inn mapfst inst_temp_defsi
⊢
Inb fn_blocksf ∧ b_labelb = d ∧ nth_errorb_instsb k = Somei ∧ j = Z.of_natk ∧ Inn mapfst inst_temp_defsi
split ; exact Hb |
split ; exact eq_symEd′ |
f :
n, d :
j :
Z
i :
b :
Hb :
Inb fn_blocksf
H :
Inn, SAtd j, DInsti inst_positionsb_labelb 0 b_instsb
k :
nat
Hk :
nth_errorb_instsb k = Somei
Ed′ :
d = b_labelb
Ej :
j = Z.of_natk
Hn :
Inn mapfst inst_temp_defsi
⊢
nth_errorb_instsb k = Somei ∧ j = Z.of_natk ∧ Inn mapfst inst_temp_defsi
split ; exact Hk |
f :
n, d :
j :
Z
i :
b :
Hb :
Inb fn_blocksf
H :
Inn, SAtd j, DInsti inst_positionsb_labelb 0 b_instsb
k :
nat
Hk :
nth_errorb_instsb k = Somei
Ed′ :
d = b_labelb
Ej :
j = Z.of_natk
Hn :
Inn mapfst inst_temp_defsi
⊢
j = Z.of_natk ∧ Inn mapfst inst_temp_defsi
split ; lia | exact Hn
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros f n d j i H
unfold def_positions in H
apply in_app_or in H as H | H
–apply in_map_iff in H as p & E & _
discriminate E
–apply in_flat_map in H as b & Hb & H
unfold block_positions in H
apply in_app_or in H as H | H
+apply in_map_iff in H as d′ k′ pairs & E & _
discriminate E
+destruct inst_positions_in_ _ _ _ _ _ H as k & i′ & Hk & Es & Ed & Hn
injection Es as Ed′ Ej
injection Ed as ←
exists b, k
split ; exact Hb |
split ; exact eq_symEd′ |
split ; exact Hk |
split ; lia | exact Hn
The instruction i at place k of a block b of f defines each of its temporaries dk at index k of b.
∀ f b k i dk
Infstdk, SAtb_labelb Z.of_natk, DInsti def_positionsf
Explore proof 11 tactics
Initial goal
intros f b k i dk Hb Hk Hdk
unfold def_positions
apply in_or_app
right
apply in_flat_map
exists b
split ; exact Hb |
unfold block_positions
apply in_or_app
right
exact inst_positions_nth_ 0 _ _ _ _ Hk Hdk
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros f b k i dk Hb Hk Hdk
unfold def_positions
apply in_or_app
right
apply in_flat_map
exists b
split ; exact Hb |
unfold block_positions
apply in_or_app
right
exact inst_positions_nth_ 0 _ _ _ _ Hk Hdk
A phi of a block b of f defines its name d at index -1 of b.
Explore proof 13 tactics
Initial goal
intros f b d k pairs Hb Hp
unfold def_positions
apply in_or_app
right
apply in_flat_map
exists b
split ; exact Hb |
unfold block_positions
apply in_or_app
left
apply in_map_iff
exists Phid k pairs
auto
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros f b d k pairs Hb Hp
unfold def_positions
apply in_or_app
right
apply in_flat_map
exists b
split ; exact Hb |
unfold block_positions
apply in_or_app
left
apply in_map_iff
exists Phid k pairs
auto
A single definition's operands are not redefined under it
Where dominance between blocks is antisymmetric, as dom_antisym gives, a site s that dominates index j of the block labelled d, where d at j dominates index k of the block labelled l, is not index k of l itself.
Explore proof 9 tactics
Initial goal
intros doms Hanti d j l k s H1 H2 →
doms :
nmapZ × Z
d :
j :
Z
l :
k :
Z
H1 :
site_dominatesdoms d j SAtl k = true
H2 :
site_dominatesdoms l k SAtd j = true
⊢
False
unfold site_dominates in H1 , H2
rewrite name_eqb_sym_dl d in H1
destruct name_eqbd l eqn: E
2 open–apply Z.ltb_lt in H1
2 openapply Z.ltb_lt in H2
2 openlia
–apply name_eqb_false in E
exact Eeq_symHanti_ _ H1 H2
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros doms Hanti d j l k s H1 H2 →
unfold site_dominates in H1 , H2
rewrite name_eqb_sym_dl d in H1
destruct name_eqbd l eqn: E
–apply Z.ltb_lt in H1
apply Z.ltb_lt in H2
lia
–apply name_eqb_false in E
exact Eeq_symHanti_ _ H1 H2
In a function f whose definitions dominate their uses, where the single definition of n by the instruction i, at index j of block d, dominates index k of a reachable block l, no operand x of i that has a single definition is defined at that index. So defining a name at a point leaves every relation in scope there between a definition and its operands' values as it was.
∀ f b0 rest doms n d j i x l k D
fn_blocksf = b0 :: rest
block_intervalsb0 :: rest = Somedoms
definitions_dominatef doms = true
lookupn single_definitionsf = SomeDInsti
Inn, SAtd j, DInsti def_positionsf
is_reachabledoms l = true
site_dominatesdoms l k SAtd j = true
Inx, SAtl k, D def_positionsf
once_hassingle_definitionsf x = true
Inx inst_usesi
False
Explore proof 17 tactics
Initial goal
⊢
∀f : func b0 : block rest : listblock doms : nmapZ × Z n d : name j : Z i : inst x l : name k : Z D : def, fn_blocksf = b0 :: rest → block_intervalsb0 :: rest = Somedoms → definitions_dominatef doms = true → lookupn single_definitionsf = SomeDInsti → Inn, SAtd j, DInsti def_positionsf → is_reachabledoms l = true → site_dominatesdoms l k SAtd j = true → Inx, SAtl k, D def_positionsf → once_hassingle_definitionsf x = true → Inx inst_usesi → False
intros f b0 rest doms n d j i x l k D Hf Hdoms Hdd Hn Hpos Hr Hsd Hx Honce Hu
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
j :
Z
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
Hpos :
Inn, SAtd j, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd j = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
⊢
False
destruct position_inst_ _ _ _ _ Hpos as b & kk & Hb & Hl & Hkk & → & _
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
⊢
False
assert Hrd : is_reachabledoms d = true
2 openf :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
⊢
is_reachabledoms d = true
focused goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms d = true
⊢
False
{unfold site_dominates in Hsd
2 openf :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
⊢
is_reachabledoms d = true
deferred goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms d = true
⊢
False
destruct name_eqbd l eqn: E
3 openf :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
E :
name_eqbd l = true
Hsd :
Z.of_natkk <? k = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
⊢
is_reachabledoms d = true
focused goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
E :
name_eqbd l = false
Hsd :
dominatesdoms d l = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
⊢
is_reachabledoms d = true
deferred goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms d = true
⊢
False
–apply name_eqb_true in E
3 openf :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
E :
d = l
Hsd :
Z.of_natkk <? k = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
⊢
is_reachabledoms d = true
deferred goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
E :
name_eqbd l = false
Hsd :
dominatesdoms d l = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
⊢
is_reachabledoms d = true
deferred goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms d = true
⊢
False
subst
3 openf :
b0 :
rest :
listblock
doms :
nmapZ × Z
n :
i :
x :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
b :
Hr :
is_reachabledoms b_labelb = true
Hpos :
Inn, SAtb_labelb Z.of_natkk, DInsti def_positionsf
Hsd :
Z.of_natkk <? k = true
Hx :
Inx, SAtb_labelb k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
Hb :
Inb fn_blocksf
Hkk :
nth_errorb_instsb kk = Somei
⊢
is_reachabledoms b_labelb = true
deferred goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
E :
name_eqbd l = false
Hsd :
dominatesdoms d l = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
⊢
is_reachabledoms d = true
deferred goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms d = true
⊢
False
exact Hr
2 opendeferred goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
E :
name_eqbd l = false
Hsd :
dominatesdoms d l = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
⊢
is_reachabledoms d = true
deferred goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms d = true
⊢
False
–exact proj1dominates_reachable_ _ _ Hdoms _ _ Hsd
deferred goal
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
once_hassingle_definitionsf x = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms d = true
⊢
False
unfold once_has in Honce
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
Honce :
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms d = true
⊢
False
destruct lookupx single_definitionsf as dx | eqn: Ex ; | discriminate Honce
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n, d :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
Hpos :
Inn, SAtd Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtd Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
dx :
Ex :
lookupx single_definitionsf = Somedx
Honce :
true = true
Hu :
Inx inst_usesi
b :
Hb :
Inb fn_blocksf
Hl :
b_labelb = d
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms d = true
⊢
False
subst d
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
b :
Hpos :
Inn, SAtb_labelb Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtb_labelb Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
dx :
Ex :
lookupx single_definitionsf = Somedx
Honce :
true = true
Hu :
Inx inst_usesi
Hb :
Inb fn_blocksf
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms b_labelb = true
⊢
False
destruct use_dominated_ _ _ _ _ _ _ Hdd Hb Hrd Hkk Hu Ex as s & Hs & Hsdom
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
b :
Hpos :
Inn, SAtb_labelb Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtb_labelb Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
dx :
Ex :
lookupx single_definitionsf = Somedx
Honce :
true = true
Hu :
Inx inst_usesi
Hb :
Inb fn_blocksf
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms b_labelb = true
s :
Hs :
Inx, s, dx def_positionsf
Hsdom :
site_dominatesdoms b_labelb Z.of_natkk s = true
⊢
False
destruct once_position_ _ _ Ex as s0 & Hs0 & Huniq
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
b :
Hpos :
Inn, SAtb_labelb Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtb_labelb Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
dx :
Ex :
lookupx single_definitionsf = Somedx
Honce :
true = true
Hu :
Inx inst_usesi
Hb :
Inb fn_blocksf
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms b_labelb = true
s :
Hs :
Inx, s, dx def_positionsf
Hsdom :
site_dominatesdoms b_labelb Z.of_natkk s = true
s0 :
Hs0 :
Inx, s0, dx def_positionsf
Huniq :
∀s′ : site d′ : def, Inx, s′, d′ def_positionsf → s′ = s0 ∧ d′ = dx
⊢
False
destruct Huniq_ _ Hs as → _
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
b :
Hpos :
Inn, SAtb_labelb Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtb_labelb Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
dx :
Ex :
lookupx single_definitionsf = Somedx
Honce :
true = true
Hu :
Inx inst_usesi
Hb :
Inb fn_blocksf
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms b_labelb = true
s0 :
Hsdom :
site_dominatesdoms b_labelb Z.of_natkk s0 = true
Hs, Hs0 :
Inx, s0, dx def_positionsf
Huniq :
∀s′ : site d′ : def, Inx, s′, d′ def_positionsf → s′ = s0 ∧ d′ = dx
⊢
False
destruct Huniq_ _ Hx as Esite _
f :
b0 :
rest :
listblock
doms :
nmapZ × Z
n :
i :
x, l :
k :
Z
D :
Hf :
fn_blocksf = b0 :: rest
Hdoms :
block_intervalsb0 :: rest = Somedoms
Hdd :
definitions_dominatef doms = true
Hn :
lookupn single_definitionsf = SomeDInsti
kk :
nat
b :
Hpos :
Inn, SAtb_labelb Z.of_natkk, DInsti def_positionsf
Hr :
is_reachabledoms l = true
Hsd :
site_dominatesdoms l k SAtb_labelb Z.of_natkk = true
Hx :
Inx, SAtl k, D def_positionsf
dx :
Ex :
lookupx single_definitionsf = Somedx
Honce :
true = true
Hu :
Inx inst_usesi
Hb :
Inb fn_blocksf
Hkk :
nth_errorb_instsb kk = Somei
Hrd :
is_reachabledoms b_labelb = true
s0 :
Hsdom :
site_dominatesdoms b_labelb Z.of_natkk s0 = true
Hs, Hs0 :
Inx, s0, dx def_positionsf
Huniq :
∀s′ : site d′ : def, Inx, s′, d′ def_positionsf → s′ = s0 ∧ d′ = dx
Esite :
SAtl k = s0
⊢
False
exact site_strictdoms dom_antisym_ _ _ Hdoms _ _ _ _ _ Hsdom Hsd eq_symEsite
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
intros f b0 rest doms n d j i x l k D Hf Hdoms Hdd Hn Hpos Hr Hsd Hx Honce Hu
destruct position_inst_ _ _ _ _ Hpos as b & kk & Hb & Hl & Hkk & → & _
assert Hrd : is_reachabledoms d = true
{unfold site_dominates in Hsd
destruct name_eqbd l eqn: E
–exact proj1dominates_reachable_ _ _ Hdoms _ _ Hsd
unfold once_has in Honce
destruct lookupx single_definitionsf as dx | eqn: Ex ; | discriminate Honce
subst d
destruct use_dominated_ _ _ _ _ _ _ Hdd Hb Hrd Hkk Hu Ex as s & Hs & Hsdom
destruct once_position_ _ _ Ex as s0 & Hs0 & Huniq
destruct Huniq_ _ Hs as → _
destruct Huniq_ _ Hx as Esite _
exact site_strictdoms dom_antisym_ _ _ Hdoms _ _ _ _ _ Hsdom Hsd eq_symEsite
Definitions that dominate a point
The dominator intervals of the function f as the validator computed them (block_intervals), or the empty map where it computed none.
Somedoms
⇒
doms
The single definition of n in f is at a site that dominates index k of the block labelled l, by the validator's intervals fn_doms.
∃s D, lookupn single_definitionsf = SomeD ∧ Inn, s, D def_positionsf ∧ site_dominatesfn_domsf l k s = true