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
d5cf327e
Commit
d5cf327e
authored
1 week ago
by
François Clément
Browse files
Options
Downloads
Patches
Plain Diff
Detection of dead code.
parent
99185901
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/geom_transf_affine.v
+36
-24
36 additions, 24 deletions
FEM/geom_transf_affine.v
with
36 additions
and
24 deletions
FEM/geom_transf_affine.v
+
36
−
24
View file @
d5cf327e
...
...
@@ -87,11 +87,12 @@ Qed.
Lemma
T_geom_vtxF
:
mapF
T_geom
vtx_ref
=
vtx
.
Proof
.
extF
;
apply
T_geom_vtx
.
Qed
.
(
*
Unused
!
Lemma
T_geom_am_lc
:
forall
L
,
sum
L
=
1
->
T_geom
(
lin_comb
L
vtx_ref
)
=
lin_comb
L
vtx
.
Proof
.
intros
;
rewrite
-!
baryc_ms_eq
// (am_normal_rev T_geom_am)// T_geom_vtxF; easy.
Qed
.
Qed
.
*
)
Lemma
T_geom_baryc
:
forall
L
,
sum
L
=
1
->
...
...
@@ -161,11 +162,12 @@ Proof. apply f_inv_can_l. Qed.
Lemma
T_geom_inv_can_r
:
cancel
T_geom_inv
(
T_geom
vtx
).
Proof
.
apply
f_inv_can_r
.
Qed
.
(
*
Unused
!
Lemma
T_geom_inv_bij
:
bijective
T_geom_inv
.
Proof
.
apply
f_inv_bij
.
Qed
.
Lemma
T_geom_inv_inj
:
injective
T_geom_inv
.
Proof
.
apply
bij_inj
,
T_geom_inv_bij
.
Qed
.
Proof
.
apply
bij_inj
,
T_geom_inv_bij
.
Qed
.
*
)
Lemma
T_geom_inv_am
:
aff_map_ms
T_geom_inv
.
Proof
.
apply
:
am_bij_compat
;
apply
T_geom_am
.
Qed
.
...
...
@@ -179,12 +181,13 @@ Proof. rewrite -(T_geom_vtxF vtx) -mapF_comp T_geom_inv_id_l; easy. Qed.
Lemma
T_geom_inv_vtx
:
forall
i
,
T_geom_inv
(
vtx
i
)
=
vtx_ref
i
.
Proof
.
intro
;
rewrite
-
T_geom_inv_vtxF
;
easy
.
Qed
.
(
*
Unused
!
Lemma
T_geom_inv_am_lc
:
forall
L
,
sum
L
=
1
->
T_geom_inv
(
lin_comb
L
vtx
)
=
lin_comb
L
vtx_ref
.
Proof
.
intros
;
rewrite
-!
baryc_ms_eq
//
(
am_normal_rev
T_geom_inv_am
)
// T_geom_inv_vtxF; easy.
Qed
.
Qed
.
*
)
Lemma
T_geom_inv_baryc
:
forall
L
,
sum
L
=
1
->
...
...
@@ -217,6 +220,7 @@ Proof.
move
=>>
[
L
HL1
HL2
];
unfold
K_geom
,
preimage
;
rewrite
T_geom_inv_baryc
;
easy
.
Qed
.
(
*
Unused
!
Lemma
T_geom_bijS_K_geom_spec
:
bijS_spec
K_geom_ref
K_geom
(
T_geom
vtx
)
(
T_geom_inv
Hvtx
).
Proof
.
...
...
@@ -241,7 +245,7 @@ intros x_ref _; apply T_geom_inv_can_l.
Qed
.
Lemma
T_geom_inv_bijS_K_geom
:
bijS
K_geom
K_geom_ref
(
T_geom_inv
Hvtx
).
Proof
.
apply
(
BijS
_
T_geom_inv_bijS_K_geom_spec
).
Qed
.
Proof
.
apply
(
BijS
_
T_geom_inv_bijS_K_geom_spec
).
Qed
.
*
)
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
...
...
@@ -339,17 +343,19 @@ Lemma T_geom_permutF_inv_can_r :
cancel
T_geom_permutF_inv
(
T_geom_permutF
vtx
pi_d
).
Proof
.
apply
f_inv_can_r
.
Qed
.
(
*
Unused
!
Lemma
T_geom_permutF_inv_id_l
:
T_geom_permutF_inv
\
o
T_geom_permutF
vtx
pi_d
=
id
.
Proof
.
apply
f_inv_id_l
.
Qed
.
Lemma
T_geom_permutF_inv_id_r
:
T_geom_permutF
vtx
pi_d
\
o
T_geom_permutF_inv
=
id
.
Proof
.
apply
f_inv_id_r
.
Qed
.
Proof
.
apply
f_inv_id_r
.
Qed
.
*
)
(
*
Unused
!
Lemma
T_geom_permutF_inv_correct
:
T_geom_permutF_inv
=
T_geom_inv
(
aff_indep_permutF
pi_d_bij
Hvtx
).
Proof
.
apply
f_inv_uniq_l
,
f_inv_can_l
.
Qed
.
Proof
.
apply
f_inv_uniq_l
,
f_inv_can_l
.
Qed
.
*
)
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
...
...
@@ -381,10 +387,11 @@ intro; unfold T_geom_permutF, T_geom;
rewrite
LagPd1_ref_sum
;
apply
invertible_one
.
Qed
.
(
*
Unused
!
Lemma
T_geom_permutF_vtx
:
forall
i
,
T_geom_permutF
vtx
pi_d
(
vtx_ref
i
)
=
T_geom
vtx
(
vtx_ref
(
pi_d
i
)).
Proof
.
intro
;
unfold
T_geom_permutF
;
rewrite
!
T_geom_vtx
;
easy
.
Qed
.
Proof
.
intro
;
unfold
T_geom_permutF
;
rewrite
!
T_geom_vtx
;
easy
.
Qed
.
*
)
Lemma
T_geom_permutF_skipF
:
forall
i
j
,
...
...
@@ -405,9 +412,10 @@ Variable vtx : 'R^{d.+1,d}.
Definition
T_geom_transpF
(
i0
:
'
I_d
.
+
1
)
:
'
R
^
d
->
'
R
^
d
:=
T_geom_permutF
vtx
(
transp_ord
ord_max
i0
).
(
*
Unused
!
Lemma
T_geom_transpF_correct
:
forall
i0
,
T_geom_transpF
i0
=
T_geom
(
transpF
ord_max
i0
vtx
).
Proof
.
easy
.
Qed
.
Proof
.
easy
.
Qed
.
*
)
End
T_geom_transpF_Def
.
...
...
@@ -440,15 +448,18 @@ Variable vtx : 'R^{d.+1,d}.
Definition
T_geom_Hface
(
i
:
'
I_d
.
+
1
)
:
'
R
^
d1
->
'
R
^
d
:=
T_geom
vtx
\
o
inj_Hface_ref
i
.
(
*
Unused
!
Lemma
T_geom_Hface_0
:
forall
{
i
}
,
i
=
ord0
->
T_geom_Hface
i
=
T_geom
vtx
\
o
part1F0
.
Proof
.
intros
;
unfold
T_geom_Hface
;
rewrite
inj_Hface_ref_0
;
easy
.
Qed
.
Proof
.
intros
;
unfold
T_geom_Hface
;
rewrite
inj_Hface_ref_0
;
easy
.
Qed
.
*
)
(
*
Unused
!
Lemma
T_geom_Hface_S
:
forall
{
i
}
(
Hi
:
i
<>
ord0
),
T_geom_Hface
i
=
T_geom
vtx
\
o
(
insert0F
^~
(
lower_S
Hi
)).
Proof
.
move
=>>
;
unfold
T_geom_Hface
;
rewrite
inj_Hface_ref_S
;
easy
.
Qed
.
Proof
.
move
=>>
;
unfold
T_geom_Hface
;
rewrite
inj_Hface_ref_S
;
easy
.
Qed
.
*
)
(
*
Unused
!
Lemma
T_geom_Hface_0_correct
:
forall
{
i
}
(
Hi
:
i
=
ord0
)
x_ref
,
T_geom_Hface
i
x_ref
=
barycenter_ms
(
LagPd1_ref
^~
x_ref
)
(
skipF
vtx
i
).
...
...
@@ -462,8 +473,9 @@ destruct (ord_eq_dec j ord0) as [-> | Hj].
rewrite
LagPd1_ref_0
// insertF_correct_l; easy.
move:
(
proj1
(
ord_n0_gt_equiv
d
)
Hj
)
=>
Hj
'
.
rewrite
LagPd1_ref_S
insertF_correct_rr
;
f_equal
;
apply
lower_S_ext
.
Qed
.
Qed
.
*
)
(
*
Unused
!
Lemma
T_geom_Hface_S_correct
:
forall
{
i
}
(
Hi
:
i
<>
ord0
)
x_ref
,
T_geom_Hface
i
x_ref
=
barycenter_ms
(
LagPd1_ref
^~
x_ref
)
(
skipF
vtx
i
).
...
...
@@ -486,9 +498,9 @@ rewrite (skip_ord_correct_l _ _ H'); apply ord_inj; simpl. admit.
(
*
*
)
assert
(
H
'
:
~
(
lower_S
Hj
<
lower_S
Hi
)
%
coq_nat
)
by
admit
.
rewrite
(
skip_ord_correct_r
_
_
H
'
);
apply
ord_inj
;
simpl
.
admit
.
Admitted
.
Admitted
.
*
)
(
*
Hopefully
,
this
should
be
useless
!
*
)
(
*
Hopefully
,
this
should
be
useless
!
Lemma
T_geom_Hface_0_lc
:
forall
x_ref
,
T_geom_Hface
ord0
x_ref
=
scal
(
1
-
sum
x_ref
)
(
vtx
ord1
)
+
...
...
@@ -496,9 +508,9 @@ Lemma T_geom_Hface_0_lc :
Proof
.
intro
;
rewrite
T_geom_Hface_0_correct
// baryc_ms_eq; [| apply LagPd1_ref_sum].
rewrite
lc_ind_l
LagPd1_ref_0
// skipF_first liftF_S_0 LagPd1_ref_SF; easy.
Qed
.
Qed
.
*
)
(
*
Hopefully
,
this
should
be
useless
!
*
)
(
*
Hopefully
,
this
should
be
useless
!
Lemma
T_geom_Hface_S_lc
:
forall
i
x_ref
,
i
<>
ord0
->
T_geom_Hface
i
x_ref
=
scal
(
1
-
sum
x_ref
)
(
vtx
ord0
)
+
...
...
@@ -508,9 +520,9 @@ intros; rewrite T_geom_Hface_S_correct// baryc_ms_eq; [| apply LagPd1_ref_sum].
assert
(
Hi
'
:
(
@
ord0
d1
<
i
)
%
coq_nat
)
by
now
apply
ord_n0_gt_equiv
.
rewrite
lc_ind_l
LagPd1_ref_0
// skipF_correct_l//
widenF_S_0
LagPd1_ref_SF
;
easy
.
Qed
.
Qed
.
*
)
(
*
Hopefully
,
this
should
be
useless
!
*
)
(
*
Hopefully
,
this
should
be
useless
!
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
Lem
1584
,
Eq
(
9.72
),
pp
.
94
-
95.
#
<
BR
>
#
...
...
@@ -524,9 +536,9 @@ Proof.
intros
;
rewrite
T_geom_Hface_0_lc
.
rewrite
scal_minus_l
scal_one
-
plus_assoc
-
minus_sym
.
rewrite
lc_minus_r
lc_constF_r
;
easy
.
Qed
.
Qed
.
*
)
(
*
Hopefully
,
this
should
be
useless
!
*
)
(
*
Hopefully
,
this
should
be
useless
!
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
Lem
1584
,
Eq
(
9.73
),
pp
.
94
-
95.
#
<
BR
>
#
...
...
@@ -540,7 +552,7 @@ Proof.
intros
;
rewrite
T_geom_Hface_S_lc
//.
rewrite
scal_minus_l
scal_one
-
plus_assoc
-
minus_sym
.
rewrite
lc_minus_r
lc_constF_r
;
easy
.
Qed
.
Qed
.
*
)
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
...
...
@@ -550,7 +562,7 @@ Proof.
intro
;
apply
am_comp_ms
;
[
apply
inj_Hface_ref_am
|
apply
T_geom_am
].
Qed
.
(
*
Hopefully
,
this
should
be
useless
!
*
)
(
*
Hopefully
,
this
should
be
useless
!
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
Lem
1584
,
Eq
(
9.73
),
pp
.
94
-
95.
#
<
BR
>
#
...
...
@@ -564,9 +576,9 @@ Proof.
intros
x_ref
;
unfold
fct_lm_ms
;
rewrite
fct_lm_ms_eq
.
rewrite
plus_zero_l
!
T_geom_Hface_0_lc_alt
lc_zero_l
plus_zero_r
.
apply:
minus_plus_l
.
Qed
.
Qed
.
*
)
(
*
Hopefully
,
this
should
be
useless
!
*
)
(
*
Hopefully
,
this
should
be
useless
!
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
Lem
1584
,
Eq
(
9.73
),
pp
.
94
-
95.
#
<
BR
>
#
...
...
@@ -580,7 +592,7 @@ Proof.
intros
i
x_ref
Hi
;
unfold
fct_lm_ms
;
rewrite
fct_lm_ms_eq
.
rewrite
plus_zero_l
!
T_geom_Hface_S_lc_alt
// lc_zero_l plus_zero_r.
apply:
minus_plus_l
.
Qed
.
Qed
.
*
)
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
...
...
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