Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
67 commits
Select commit Hold shift + click to select a range
0e4fff0
upd opam
affeldt-aist Nov 17, 2025
adb18ab
start tilt formalization
affeldt-aist May 26, 2025
950fa8d
basic facts update (#44)
yosakaon Jun 2, 2025
a49797e
equilibrium point
affeldt-aist Jun 2, 2025
a0dce21
started lyapunov function formalization
yosakaon Jun 16, 2025
3ce694e
fixes
affeldt-aist Jun 16, 2025
8e46613
update lyapunov
yosakaon Jun 16, 2025
3acd218
fix
affeldt-aist Jun 16, 2025
84b3d19
derive norm lemma
yosakaon Jun 18, 2025
6f85a58
wip
affeldt-aist Jun 18, 2025
6823d0c
upd
yosakaon Jun 19, 2025
75cc1ce
wip
affeldt-aist Jun 19, 2025
d5be328
working on is lyapunov
yosakaon Jun 20, 2025
bd98bad
upd
yosakaon Jun 23, 2025
06e06b6
cleaning, wip
affeldt-aist Jun 23, 2025
b11aed6
proved V1 Lie derivative matches the one in the paper + LieDerivative…
yosakaon Jun 26, 2025
345d71d
fix naming
yosakaon Jun 27, 2025
a659974
working towards the end of the proof v1 is a lyapunov fx
yosakaon Jul 4, 2025
dcecff0
derive_sqrt and norm update
yosakaon Jul 7, 2025
7eb5245
complete proof of defposmx and such
yosakaon Jul 9, 2025
849ad48
refactoring
yosakaon Jul 15, 2025
ef73944
clean
yosakaon Jul 16, 2025
5849da8
upd
yosakaon Jul 18, 2025
edf2c77
proved derivative is equal to 0 + bureaucratie lsubmx/rsubmx
yosakaon Jul 21, 2025
90684b1
upd
yosakaon Jul 22, 2025
a57165c
proved first implication of thm11a
yosakaon Jul 22, 2025
c51cb26
preuve thm11a sans cauchy
yosakaon Jul 23, 2025
679677f
cleaning
affeldt-aist Jul 23, 2025
28be66e
tentative d'enonce
yosakaon Jul 28, 2025
4620af5
split file
affeldt-aist Jul 28, 2025
c44d663
cleaning + towards context formalization
yosakaon Jul 30, 2025
02e32ce
getting rid of admits (wip)
affeldt-aist Jul 30, 2025
3034e3e
upd
yosakaon Jul 31, 2025
6343c50
bricolage y_a
affeldt-aist Jul 31, 2025
5a98bbe
upd
yosakaon Jul 31, 2025
df87911
less admits
affeldt-aist Aug 3, 2025
cb67e17
part 3B
yosakaon Aug 1, 2025
419c47e
velocity is not derived anymore but a measure
yosakaon Aug 6, 2025
56f59ba
checkpoint
yosakaon Aug 6, 2025
9e25f85
working state
yosakaon Aug 6, 2025
a41bbff
fix solves_equations
yosakaon Aug 8, 2025
be84908
rocq 9 update
yosakaon Aug 8, 2025
4fbdd8e
frames + diff
yosakaon Aug 13, 2025
d66c8d1
upd
yosakaon Aug 14, 2025
8d90d73
a few lemmas about derivation
affeldt-aist Aug 14, 2025
a30ecb2
propagate deriv hypo (broken state)
yosakaon Aug 14, 2025
c6de020
cleaning
yosakaon Aug 15, 2025
f19ef25
wip lyapunov + closed ball
yosakaon Aug 29, 2025
c3f26b1
use closed_ball_
affeldt-aist Sep 11, 2025
8c148dc
wip lyapunov
yosakaon Sep 12, 2025
85ff05e
fix compilation of tilt.v
yosakaon Sep 19, 2025
1fc7ff8
doc formatting, cleaning
affeldt-aist Sep 19, 2025
82addd5
remove differentiability admits
yosakaon Oct 5, 2025
a790c5b
renaming of part A
yosakaon Oct 7, 2025
c3ab00a
removed continuity admits from lyapunov proof
yosakaon Oct 7, 2025
704b834
fix notation
yosakaon Oct 8, 2025
93e501a
trying to prove 0 is stable
yosakaon Oct 8, 2025
b688fc9
progress, cleaning, fix
affeldt-aist Oct 8, 2025
46b75c2
upd lnd
yosakaon Oct 10, 2025
90b3f7f
fix derive norm squared
affeldt-aist Oct 10, 2025
dd6edbd
progress lyapunov application
yosakaon Oct 13, 2025
12427ab
evt for rV
affeldt-aist Oct 13, 2025
a45dd22
finished lyapunov
yosakaon Oct 14, 2025
edd859e
various fixes:
affeldt-aist Oct 14, 2025
e787325
cleaning of tilt files
yosakaon Dec 4, 2025
7734d52
minor renaming
affeldt-aist Dec 4, 2025
19c1aa3
minor cleaning
yosakaon Dec 5, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ jobs:
fail-fast: false
steps:
- uses: actions/checkout@v2
- uses: coq-community/docker-coq-action@v1
- uses: rocq-community/docker-rocq-action@v1
with:
opam_file: 'robot-rocq.opam'
custom_image: ${{ matrix.image }}
Expand Down
5 changes: 5 additions & 0 deletions _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -17,5 +17,10 @@ scara.v
derive_matrix.v
differential_kinematics.v
extra_trigo.v
tilt_mathcomp.v
tilt_analysis.v
tilt_robot.v
tilt.v


-R . robot
Loading
Loading