Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
N
Numerical Analysis in Coq
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Micaela Mayero
Numerical Analysis in Coq
Commits
c58faad6
Commit
c58faad6
authored
1 week ago
by
François Clément
Browse files
Options
Downloads
Patches
Plain Diff
Detection of dead code.
parent
e65339a5
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
FEM/poly_LagPd1.v
+38
-21
38 additions, 21 deletions
FEM/poly_LagPd1.v
with
38 additions
and
21 deletions
FEM/poly_LagPd1.v
+
38
−
21
View file @
c58faad6
...
...
@@ -60,11 +60,13 @@ Proof. easy. Qed.
Lemma
LagPd1_eqF
:
LagPd1
=
compF_l
LagPd1_ref
(
T_geom_inv
Hvtx
).
Proof
.
easy
.
Qed
.
(
*
Unused
!
Lemma
LagPd1_ref_eq
:
forall
i
,
LagPd1_ref
i
=
LagPd1
i
\
o
(
T_geom
vtx
).
Proof
.
intro
;
rewrite
LagPd1_eq
-
comp_assoc
T_geom_inv_id_l
;
easy
.
Qed
.
Proof
.
intro
;
rewrite
LagPd1_eq
-
comp_assoc
T_geom_inv_id_l
;
easy
.
Qed
.
*
)
(
*
Unused
!
Lemma
LagPd1_ref_eqF
:
LagPd1_ref
=
compF_l
LagPd1
(
T_geom
vtx
).
Proof
.
extF
;
apply
LagPd1_ref_eq
.
Qed
.
Proof
.
extF
;
apply
LagPd1_ref_eq
.
Qed
.
*
)
Lemma
LagPd1_0
:
forall
i
,
i
=
ord0
->
LagPd1
i
=
fun
x
=>
1
-
sum
(
T_geom_inv
Hvtx
x
).
...
...
@@ -84,16 +86,19 @@ intro; extF; unfold liftF_S.
rewrite
(
LagPd1_S
(
lift_S_not_first
_
))
lower_lift_S
;
easy
.
Qed
.
(
*
Unused
!
Lemma
LagPd1_S_eq_f
:
(
fun
x
=>
liftF_S
(
LagPd1
^~
x
))
=
T_geom_inv
Hvtx
.
Proof
.
fun_ext
;
apply
LagPd1_S_eq
.
Qed
.
Proof
.
fun_ext
;
apply
LagPd1_S_eq
.
Qed
.
*
)
(
*
Unused
!
Lemma
LagPd1_0_eq
:
forall
{
i
}
x
,
i
=
ord0
->
LagPd1
i
x
=
1
-
sum
(
liftF_S
(
LagPd1
^~
x
)).
Proof
.
intros
;
subst
;
rewrite
LagPd1_0
// LagPd1_S_eq; easy. Qed.
Proof
.
intros
;
subst
;
rewrite
LagPd1_0
// LagPd1_S_eq; easy. Qed.
*)
(
*
Unused
!
Lemma
LagPd1_0_eq_f
:
forall
{
i
}
,
i
=
ord0
->
LagPd1
i
=
1
-
fun
x
=>
sum
(
liftF_S
(
LagPd1
^~
x
)).
Proof
.
intros
;
fun_ext
;
apply
LagPd1_0_eq
;
easy
.
Qed
.
Proof
.
intros
;
fun_ext
;
apply
LagPd1_0_eq
;
easy
.
Qed
.
*
)
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
...
...
@@ -107,18 +112,20 @@ Proof. intro; rewrite LagPd1_S_eq; apply T_geom_inv_can_l. Qed.
Lemma
LagPd1_S_can_r
:
forall
x
,
T_geom
vtx
(
liftF_S
(
LagPd1
^~
x
))
=
x
.
Proof
.
intro
;
rewrite
LagPd1_S_eq
;
apply
T_geom_inv_can_r
.
Qed
.
(
*
Unused
!
(
*
Could
be
:
injective
(
gather
LagPd1
).
*
)
Lemma
LagPd1_inj
:
forall
(
x
y
:
'
R
^
d
),
(
forall
i
,
LagPd1
i
x
=
LagPd1
i
y
)
->
x
=
y
.
Proof
.
move
=>>
/
LagPd1_ref_inj
/
T_geom_inv_inj
;
easy
.
Qed
.
Proof
.
move
=>>
/
LagPd1_ref_inj
/
T_geom_inv_inj
;
easy
.
Qed
.
*
)
(
*
Unused
!
(
*
Could
be
:
surjS
fullset
(
fun
L
=>
sum
L
=
1
)
(
fun
x
=>
LagPd1
^~
x
).
*
)
Lemma
LagPd1_surjS
:
forall
(
L
:
'
R
^
d
.
+
1
),
sum
L
=
1
->
exists
x
,
LagPd1
^~
x
=
L
.
Proof
.
intros
L
HL
;
exists
(
T_geom
vtx
(
liftF_S
L
)).
unfold
LagPd1
;
rewrite
T_geom_inv_can_l
LagPd1_ref_liftF_S
;
easy
.
Qed
.
Qed
.
*
)
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
...
...
@@ -126,22 +133,25 @@ Qed.
Lemma
LagPd1_sum
:
forall
x
,
sum
(
LagPd1
^~
x
)
=
1.
Proof
.
intros
;
apply
LagPd1_ref_sum
.
Qed
.
(
*
Unused
!
Lemma
LagPd1_sum_f
:
sum
LagPd1
=
1.
Proof
.
fun_ext
;
rewrite
fct_sum_eq
LagPd1_sum
;
easy
.
Qed
.
Proof
.
fun_ext
;
rewrite
fct_sum_eq
LagPd1_sum
;
easy
.
Qed
.
*
)
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
Lem
1554
,
Eq
(
9.45
),
p
.
85.
*
)
Lemma
LagPd1_kron_vtx
:
forall
i
j
,
LagPd1
j
(
vtx
i
)
=
kronR
i
j
.
Lemma
LagPd1_kron_vtx
:
forall
i
,
LagPd1
^~
(
vtx
i
)
=
kronR
i
.
Proof
.
intros
;
unfold
LagPd1
;
rewrite
T_geom_inv_vtx
;
apply
LagPd1_ref_kron_vtx
.
intros
;
extF
;
unfold
LagPd1
;
rewrite
T_geom_inv_vtx
;
apply
LagPd1_ref_kron_vtx
.
Qed
.
(
*
Unused
!
Lemma
LagPd1_kron_vtx_r
:
forall
i
,
LagPd1
^~
(
vtx
i
)
=
kronR
i
.
Proof
.
intro
;
extF
;
apply
LagPd1_kron_vtx
.
Qed
.
Proof
.
intro
;
extF
;
apply
LagPd1_kron_vtx
.
Qed
.
*
)
(
*
Unused
!
Lemma
LagPd1_kron_vtx_l
:
forall
j
,
mapF
(
LagPd1
j
)
vtx
=
kronR
^~
j
.
Proof
.
intro
;
extF
;
rewrite
mapF_correct
;
apply
LagPd1_kron_vtx
.
Qed
.
Proof
.
intro
;
extF
;
rewrite
mapF_correct
;
apply
LagPd1_kron_vtx
.
Qed
.
*
)
Lemma
LagPd1_am
:
forall
i
,
aff_map_ms
(
LagPd1
i
).
Proof
.
...
...
@@ -162,10 +172,11 @@ intros; eapply am_ext.
easy
.
Qed
.
(
*
Unused
!
Lemma
LagPd1_am_lc
:
forall
L
i
,
sum
L
=
1
->
LagPd1
i
(
lin_comb
L
vtx
)
=
L
i
.
Proof
.
intros
;
unfold
LagPd1
;
rewrite
T_geom_inv_am_lc
// LagPd1_ref_baryc_lc; easy.
Qed
.
Qed
.
*
)
Let
K_geom
:
'
R
^
d
->
Prop
:=
convex_envelop
vtx
.
...
...
@@ -184,26 +195,30 @@ Proof.
intros
x
;
rewrite
-{
2
}
(
LagPd1_S_can_r
x
);
unfold
T_geom
;
rewrite
LagPd1_S_eq
//.
Qed
.
(
*
Unused
!
Lemma
LagPd1_baryc_rev
:
forall
L
,
sum
L
=
1
->
LagPd1
^~
(
barycenter_ms
L
vtx
)
=
L
.
Proof
.
intros
;
extF
j
;
rewrite
(
am_normal_rev
(
LagPd1_am
j
))
//.
rewrite
LagPd1_kron_vtx_l
;
apply
baryc_r_kron_l
;
easy
.
Qed
.
Qed
.
*
)
(
*
Unused
!
Lemma
LagPd1_baryc_alt
:
forall
x
L
,
L
=
LagPd1
^~
x
->
barycenter_ms
L
vtx
=
x
.
Proof
.
intros
;
subst
;
apply
LagPd1_baryc
.
Qed
.
Proof
.
intros
;
subst
;
apply
LagPd1_baryc
.
Qed
.
*
)
(
*
Unused
!
Lemma
LagPd1_baryc_rev_alt
:
forall
x
L
,
sum
L
=
1
->
x
=
barycenter_ms
L
vtx
->
LagPd1
^~
x
=
L
.
Proof
.
intros
;
subst
;
apply
LagPd1_baryc_rev
;
easy
.
Qed
.
Proof
.
intros
;
subst
;
apply
LagPd1_baryc_rev
;
easy
.
Qed
.
*
)
(
*
Unused
!
Lemma
LagPd1_baryc_equiv
:
forall
x
L
,
sum
L
=
1
->
x
=
barycenter_ms
L
vtx
<->
LagPd1
^~
x
=
L
.
Proof
.
intros
;
split
;
intros
;
subst
;
[
apply
LagPd1_baryc_rev_alt
|
apply
eq_sym
,
LagPd1_baryc_alt
];
easy
.
Qed
.
Qed
.
*
)
Lemma
LagPd1_is_Pd1
:
inclF
LagPd1
(
Pdk
d
1
).
Proof
.
...
...
@@ -214,7 +229,7 @@ Qed.
Lemma
LagPd1_lin_indep
:
lin_indep
LagPd1
.
Proof
.
intros
L
HL
;
extF
;
rewrite
-
lc_r_kron_r
.
rewrite
-
LagPd1_kron_vtx
_r
-
fct_lc_r_eq
HL
;
easy
.
rewrite
-
LagPd1_kron_vtx
-
fct_lc_r_eq
HL
;
easy
.
Qed
.
(
**
...
...
@@ -233,7 +248,7 @@ Lemma LagPd1_decomp_vtx :
forall
{
p
}
,
Pdk
d
1
p
->
p
=
lin_comb
(
mapF
p
vtx
)
LagPd1
.
Proof
.
intros
p
Hp
;
destruct
(
basis_decomp_ex
LagPd1_basis
p
Hp
)
as
[
L
->
].
apply
lc_ext_l
;
intro
;
rewrite
mapF_correct
fct_lc_r_eq
LagPd1_kron_vtx
_r
.
apply
lc_ext_l
;
intro
;
rewrite
mapF_correct
fct_lc_r_eq
LagPd1_kron_vtx
.
apply
eq_sym
,
lc_r_kron_r
.
Qed
.
...
...
@@ -479,6 +494,7 @@ rewrite (LagPd1_eq_transpF _ i) transpF_correct_l1//
-
f_mult_compat_comp_l
-
Hq2
;
easy
.
Qed
.
(
*
Unused
!
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
Lem
1623
,
reverse
way
,
p
.
105.
*
)
...
...
@@ -489,8 +505,9 @@ Lemma factor_zero_on_Hface_rev :
Proof
.
move
=>>
Hp
[
q
[
Hq
->
]]
=>>
;
rewrite
Hface_is_Ker
=>
Hx
.
rewrite
fct_mult_eq
Hx
mult_zero_l
;
easy
.
Qed
.
Qed
.
*
)
(
*
Unused
!
Lemma
factor_zero_on_Hface_equiv
:
forall
{
p
}
i
,
Pdk
d
k
.
+
1
p
->
(
forall
x
,
Hface
vtx
i
x
->
p
x
=
0
)
<->
...
...
@@ -498,7 +515,7 @@ Lemma factor_zero_on_Hface_equiv :
Proof
.
intros
;
split
;
[
apply
factor_zero_on_Hface
|
apply
factor_zero_on_Hface_rev
];
easy
.
Qed
.
Qed
.
*
)
End
Pdk_Facts
.
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment