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
42637351
Commit
42637351
authored
1 week ago
by
François Clément
Browse files
Options
Downloads
Patches
Plain Diff
Detection of dead code.
parent
5ce84066
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
FEM/LagP_node_ref.v
+14
-8
14 additions, 8 deletions
FEM/LagP_node_ref.v
with
14 additions
and
8 deletions
FEM/LagP_node_ref.v
+
14
−
8
View file @
42637351
...
...
@@ -88,6 +88,7 @@ intros idk jdk; rewrite !node_ref_eqF;
move
=>
/
(
scal_reg_r_R
_
(
INR_inv_n0
Hk
))
/
(
mapF_inj
INR_eq
)
/
Adk_inj
;
easy
.
Qed
.
(
*
Unused
!
Lemma
vtx_node_ref
:
(
0
<
k
)
%
coq_nat
->
invalF
vtx_ref
node_ref
.
Proof
.
intros
Hk
i
;
destruct
(
ord_eq_dec
i
ord0
)
as
[
->
|
Hi
].
...
...
@@ -96,7 +97,7 @@ exists (Adk_inv d k (itemF d k (lower_S Hi)));
rewrite
vtx_ref_S
node_ref_eqF
Adk_kron
.
extF
j
;
rewrite
fct_scal_eq
scal_eq_K
mult_assoc
(
mult_inv_l
(
INR_invertible
Hk
))
mult_one_l
;
easy
.
Qed
.
Qed
.
*
)
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
...
...
@@ -118,13 +119,14 @@ Lemma node_ref_Hface_ref_S :
Hface_ref
i
(
node_ref
idk
)
<->
Adk
d
k
idk
(
lower_S
Hi
)
=
O
.
Proof
.
intros
;
rewrite
Hface_ref_S_eq
;
apply
node_ref_ASdki
;
easy
.
Qed
.
(
*
Unused
!
Lemma
node_ref_Hface_ref_S_old
:
forall
(
idk
:
'
I_
((
pbinom
d
k
).
+
1
))
(
i
:
'
I_d
),
(
0
<
d
)
%
coq_nat
->
(
0
<
k
)
%
coq_nat
->
Hface_ref
(
lift_S
i
)
(
node_ref
idk
)
<->
Adk
d
k
idk
i
=
O
.
Proof
.
intros
;
rewrite
(
node_ref_Hface_ref_S
_
(
lift_S_not_first
_
))
// lower_lift_S//.
Qed
.
Qed
.
*
)
End
Node_ref_Facts1
.
...
...
@@ -187,14 +189,14 @@ Qed.
Lemma
node_vtx_ref_d1
:
node_ref
=
castF
(
eq_sym
(
pbinomS_1_r
d
))
vtx_ref
.
Proof
.
intros
;
rewrite
eq_sym_equiv
-
castF_sym_equiv
-
vtx_node_ref_d1
//. Qed.
(
*
Useless
?
*
)
(
*
Useless
!
Lemma
LagPd1_ref_decomp_node
:
forall
{
p
}
,
Pdk
d
1
p
->
p
=
lin_comb
(
mapF
p
node_ref
)
(
castF
(
eq_sym
(
pbinomS_1_r
d
))
LagPd1_ref
).
Proof
.
intro
;
rewrite
node_vtx_ref_d1
mapF_castF
lc_castF
;
apply
LagPd1_ref_decomp_vtx
.
Qed
.
Qed
.
*
)
End
Node_ref_d1
.
...
...
@@ -214,6 +216,7 @@ Variable vtx : 'R^{d.+1,d}.
Definition
sub_vtx_ref
:
'
I_d
.
+
1
->
'
R
^
d
:=
mapF
(
scal
(
INR
k
.
-
1
/
INR
k
))
vtx_ref
.
(
*
Unused
!
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
Def
1594
(
for
[
vtx_ref
]
and
i
=
0
),
Eq
(
9.88
),
p
.
98.
#
<
BR
>
#
...
...
@@ -222,8 +225,9 @@ Lemma sub_vtx_ref_0 : forall {i}, i = ord0 -> sub_vtx_ref i = vtx_ref ord0.
Proof
.
intros
;
subst
;
unfold
sub_vtx_ref
;
rewrite
mapF_correct
vtx_ref_0
// scal_zero_r; easy.
Qed
.
Qed
.
*
)
(
*
Unused
!
(
**
#
<
A
HREF
=
"##RR9557v1"
>
#[[
RR9557v1
]]#
</
A
>
#
Def
1594
(
for
[
vtx_ref
]
and
i
<>
0
),
Eq
(
9.88
),
p
.
98.
#
<
BR
>
#
...
...
@@ -237,22 +241,24 @@ intros Hk i Hi; unfold sub_vtx_ref; rewrite node_ref_eqF Adk_inv_correct_r//;
rewrite
mapF_itemF_0
;
[
|
apply
INR_0
];
extF
j
.
rewrite
itemF_kron_eq
!
fct_scal_eq
-
scal_eq_K
scal_assoc
mult_comm_R
.
rewrite
mapF_correct
vtx_ref_S
div_eq
;
easy
.
Qed
.
Qed
.
*
)
(
*
Unused
!
Lemma
LagPd1_ref_sub_vtx_0
:
forall
i
,
i
=
ord0
->
LagPd1_ref
^~
(
sub_vtx_ref
i
)
=
itemF
d
.
+
1
1
i
.
Proof
.
intros
;
subst
;
rewrite
sub_vtx_ref_0
// LagPd1_ref_kron_vtx_r itemF_kron_eq.
extF
j
;
rewrite
mult_one_l
;
easy
.
Qed
.
Qed
.
*
)
(
*
Unused
!
Lemma
LagPd1_ref_sub_vtx
:
(
0
<
k
)
%
coq_nat
->
forall
i
,
i
<>
ord0
->
LagPd1_ref
^~
(
sub_vtx_ref
i
)
=
itemF
d
.
+
1
(
INR
k
.
-
1
/
INR
k
)
i
.
Proof
.
intros
;
rewrite
sub_vtx_ref_S
//.
Admitted
.
Admitted
.
*
)
End
Sub_vertices_ref_Def
.
...
...
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