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
Compare revisions
4c24d9b587f76a6697e9f8a773dc319396f3f2ef to a3e3422f676102dca0c593e2f7a62ac32fac9340
Compare revisions
Changes are shown as if the
source
revision was being merged into the
target
revision.
Learn more about comparing revisions.
Source
mayero/coq-num-analysis
Select target project
No results found
a3e3422f676102dca0c593e2f7a62ac32fac9340
Select Git revision
Swap
Target
mayero/coq-num-analysis
Select target project
mayero/coq-num-analysis
hamelin/test-ci-coq-num-analysis
arias/coq-num-analysis
3 results
4c24d9b587f76a6697e9f8a773dc319396f3f2ef
Select Git revision
Show changes
Only incoming changes from source
Include changes to target since source was created
Compare
Commits on Source (2)
WIP: rev_insert_ord.
· e242e931
François Clément
authored
3 days ago
Proof of insertF_revF.
e242e931
Add nat_sub_r_monot,
· a3e3422f
François Clément
authored
3 days ago
rev_ord_monot. Proof of rev_insert_ord.
a3e3422f
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
Numbers/nat_compl.v
+5
-0
5 additions, 0 deletions
Numbers/nat_compl.v
Subsets/Finite_family.v
+7
-4
7 additions, 4 deletions
Subsets/Finite_family.v
Subsets/ord_compl.v
+20
-0
20 additions, 0 deletions
Subsets/ord_compl.v
with
32 additions
and
4 deletions
Numbers/nat_compl.v
View file @
a3e3422f
...
@@ -302,6 +302,11 @@ Lemma nat_sub2_r :
...
@@ -302,6 +302,11 @@ Lemma nat_sub2_r :
forall
m
n
,
(
n
<=
m
)
%
coq_nat
->
(
m
-
(
m
-
n
)
%
coq_nat
)
%
coq_nat
=
n
.
forall
m
n
,
(
n
<=
m
)
%
coq_nat
->
(
m
-
(
m
-
n
)
%
coq_nat
)
%
coq_nat
=
n
.
Proof
.
lia
.
Qed
.
Proof
.
lia
.
Qed
.
Lemma
nat_sub_r_monot
:
forall
m
n
p
,
(
m
<=
p
)
%
coq_nat
->
(
n
<=
p
)
%
coq_nat
->
(
m
<
n
)
%
coq_nat
->
((
p
-
n
)
%
coq_nat
<
(
p
-
m
)
%
coq_nat
)
%
coq_nat
.
Proof
.
lia
.
Qed
.
Lemma
nat_double_S
:
forall
n
,
(
2
*
n
.
+
1
)
%
coq_nat
=
(
2
*
n
)
%
coq_nat
.
+
2.
Lemma
nat_double_S
:
forall
n
,
(
2
*
n
.
+
1
)
%
coq_nat
=
(
2
*
n
)
%
coq_nat
.
+
2.
Proof
.
intros
;
rewrite
Nat
.
mul_succ_r
;
apply
nat_add_2_r
.
Qed
.
Proof
.
intros
;
rewrite
Nat
.
mul_succ_r
;
apply
nat_add_2_r
.
Qed
.
...
...
This diff is collapsed.
Click to expand it.
Subsets/Finite_family.v
View file @
a3e3422f
...
@@ -4413,10 +4413,13 @@ Lemma insertF_revF :
...
@@ -4413,10 +4413,13 @@ Lemma insertF_revF :
forall
{
n
}
i0
x0
(
A
:
'
E
^
n
),
forall
{
n
}
i0
x0
(
A
:
'
E
^
n
),
insertF
i0
x0
(
revF
A
)
=
revF
(
insertF
(
rev_ord
i0
)
x0
A
).
insertF
i0
x0
(
revF
A
)
=
revF
(
insertF
(
rev_ord
i0
)
x0
A
).
Proof
.
Proof
.
intros
;
rewrite
(
insertF_permutF
rev_ord_inj
).
unfold
revF
.
intros
n
i0
x0
A
;
rewrite
(
insertF_permutF
rev_ord_inj
);
unfold
revF
.
extF
i
;
rewrite
!
permutF_correct
;
destruct
(
ord_eq_dec
i
i0
)
as
[
->
|
Hi
].
rewrite
insert_f_ord_correct_l
// !insertF_correct_l//.
Admitted
.
move:
(
skip_ord_correct_m
i0
)
(
inj_contra
rev_ord_inj
_
_
Hi
)
=>
H1
H2
.
rewrite
insert_f_ord_correct_r
!
insertF_correct_r
insert_skip_ord
rev_insert_ord
;
easy
.
Qed
.
Lemma
revF_insertF
:
Lemma
revF_insertF
:
forall
{
n
}
i0
x0
(
A
:
'
E
^
n
),
forall
{
n
}
i0
x0
(
A
:
'
E
^
n
),
...
...
This diff is collapsed.
Click to expand it.
Subsets/ord_compl.v
View file @
a3e3422f
...
@@ -2431,6 +2431,26 @@ Proof. intros; apply injF_surj, rev_ord_inj. Qed.
...
@@ -2431,6 +2431,26 @@ Proof. intros; apply injF_surj, rev_ord_inj. Qed.
Lemma
rev_ord_max
:
forall
{
n
}
,
rev_ord
(
@
ord_max
n
)
=
ord0
.
Lemma
rev_ord_max
:
forall
{
n
}
,
rev_ord
(
@
ord_max
n
)
=
ord0
.
Proof
.
intros
;
apply
ord_inj
;
simpl
;
apply
subnn
.
Qed
.
Proof
.
intros
;
apply
ord_inj
;
simpl
;
apply
subnn
.
Qed
.
Lemma
rev_ord_monot
:
forall
{
n
}
{
i
j
:
'
I_n
}
,
(
i
<
j
)
%
coq_nat
->
(
rev_ord
j
<
rev_ord
i
)
%
coq_nat
.
Proof
.
move
=>>
H
;
rewrite
!
rev_ord_correct
-
minusE
;
apply
nat_sub_r_monot
;
[
apply
/
leP
..
|
rewrite
-
Nat
.
succ_lt_mono
];
easy
.
Qed
.
Lemma
rev_insert_ord
:
forall
{
n
}
{
i0
i
:
'
I_n
.
+
1
}
(
H1
:
i
<>
i0
)
(
H2
:
rev_ord
i
<>
rev_ord
i0
),
rev_ord
(
insert_ord
H1
)
=
insert_ord
H2
.
Proof
.
intros
n
i0
i
H1
H2
;
destruct
(
lt_eq_lt_dec
i
i0
)
as
[[
H3
|
H3
]
|
H3
];
[
|
contradict
H1
;
apply
ord_inj
;
easy
|
];
move:
(
rev_ord_monot
H3
)
=>
H4
.
rewrite
insert_ord_correct_l
insert_ord_correct_r
;
apply
ord_inj
;
simpl
.
rewrite
-
minusE
;
lia
.
rewrite
insert_ord_correct_r
insert_ord_correct_l
;
apply
ord_inj
;
simpl
.
rewrite
-
minusE
;
lia
.
Qed
.
Lemma
cast_f_rev_ord
:
Lemma
cast_f_rev_ord
:
forall
{
n1
n2
}
(
H
:
n1
=
n2
),
cast_f_ord
H
(
@
rev_ord
n1
)
=
@
rev_ord
n2
.
forall
{
n1
n2
}
(
H
:
n1
=
n2
),
cast_f_ord
H
(
@
rev_ord
n1
)
=
@
rev_ord
n2
.
Proof
.
intros
;
subst
;
fun_ext
;
apply
ord_inj
;
easy
.
Qed
.
Proof
.
intros
;
subst
;
fun_ext
;
apply
ord_inj
;
easy
.
Qed
.
...
...
This diff is collapsed.
Click to expand it.