104 lines
1.8 KiB
Coq
104 lines
1.8 KiB
Coq
(* ** Strictly decreasing [list nat] *)
|
|
|
|
(*
|
|
l MAX: non empty list
|
|
|
|
l n
|
|
| start: l n
|
|
| cons: n >= m ->
|
|
|
|
|
|
|
repeat:
|
|
| Repeat: forall n>1 ∧ n<4, tok -> repeat
|
|
|
|
repeat:
|
|
| R1one: one -> repeat
|
|
| R1oth: other -> repeat
|
|
| R2: other -> repeat
|
|
| R3: other -> repeat.
|
|
|
|
*)
|
|
Inductive foo: nat -> nat -> Type :=
|
|
| Foo: forall n m:nat, n > m -> foo n m.
|
|
|
|
Inductive bar: nat -> Type :=
|
|
| Bar: forall n:nat, bar n.
|
|
|
|
Inductive decrList: nat -> Type :=
|
|
| DEmpty: decrList 0
|
|
| DCons: forall n m:nat,
|
|
foo n m -> bar m -> decrList n -> decrList m.
|
|
|
|
Check DCons 0 0 (Foo _ _ _) (Bar _) DEmpty.
|
|
Check DCons 3 0 (Foo _ _ _) (Bar _).
|
|
|
|
|
|
(*
|
|
pre := I | X | C
|
|
one := D | L | V
|
|
thrice := M | pre
|
|
all := M | pre | once
|
|
|
|
-----
|
|
|
|
subpair := IV | IX
|
|
XL | XC
|
|
CD | CM
|
|
one := D | L | V
|
|
|
|
No symbol occurs more than thrice consecutively: https://www.numere-romane.ro/rule2-repetition-of-basic-symbols-in-roman-numerals.php?lang=en
|
|
|
|
MCX use instead of:
|
|
'M, C, and X cannot be equalled or exceeded by smaller denominations.'
|
|
- X: VV
|
|
- M: C * 10 ✓
|
|
- C: X * 10 ✓
|
|
|
|
num := all
|
|
|
|
additive notation, subtractive notation
|
|
*)
|
|
|
|
Inductive other: Set := V | L | D | M.
|
|
Inductive subpre := I | X | C.
|
|
Inductive tok: Set :=
|
|
| Other: other -> tok
|
|
| SubPre: subpre -> tok.
|
|
|
|
Definition val (n:tok): nat :=
|
|
match n with
|
|
| Other x =>
|
|
match x with
|
|
| V => 5
|
|
| L => 50
|
|
| D => 500
|
|
| M => 1000
|
|
end
|
|
| SubPre x =>
|
|
match x with
|
|
| I => 1
|
|
| X => 10
|
|
| C => 100
|
|
end
|
|
end.
|
|
|
|
|
|
Inductive rnumSub: Set :=
|
|
| RSub: subpre -> tok -> rnumSub.
|
|
|
|
Inductive rnum: Type :=
|
|
| RNil: rnum
|
|
| RCons: other -> rnum -> rnum
|
|
| RSubCons: rnumSub -> rnum -> rnum.
|
|
|
|
(*
|
|
CDXCIX
|
|
|
|
|
|
*)
|
|
Example eg1 := RSub I (SubPre X). (* IX *)
|
|
Example eg2 := RSub X (SubPre C). (* XC *)
|
|
Example eg3 := RSub C (Other D). (* XC *)
|
|
|
|
|