the next generation of the in-browser educational proof assistant
Merge pull request #12 from mio-19/main
Derived Induction Rules
authored by
Liam O'Connor
and committed by
GitHub
e654f82e
61c58dd9
+718
-4
+27
index.html
+27
index.html
···
257
257
</style>
258
258
</head>
259
259
<body>
260
+
<hol-inductive id="index.html/nat" deps="index.html/myconfig">
261
+
---- Z
262
+
(Nat 0)
263
+
264
+
n.
265
+
(Nat n)
266
+
------- S
267
+
(Nat (S n))
268
+
269
+
---- even-0
270
+
(Even 0)
271
+
n.
272
+
(Even n)
273
+
-------- odd
274
+
(Odd (S n))
275
+
n.
276
+
(Odd n)
277
+
------- even
278
+
(Even (S n))
279
+
280
+
---- Unit
281
+
(Data U)
282
+
a. b.
283
+
(Data a) (Data b)
284
+
---- Pair
285
+
(Data (A a b))
286
+
</hol-inductive>
260
287
<hol-comp id="index.html/baz" deps="index.html/myconfig">
261
288
x.y.
262
289
(/\ x y)
+439
-3
package-lock.json
+439
-3
package-lock.json
···
25
25
"eslint-plugin-react-hooks": "^5.2.0",
26
26
"eslint-plugin-react-refresh": "^0.4.19",
27
27
"globals": "^16.0.0",
28
+
"husky": "^9.1.7",
29
+
"lint-staged": "^16.2.3",
28
30
"onchange": "^7.1.0",
29
31
"pta": "^1.3.0",
30
32
"typescript": "~5.8.3",
···
1658
1660
"url": "https://github.com/sponsors/epoberezkin"
1659
1661
}
1660
1662
},
1663
+
"node_modules/ansi-escapes": {
1664
+
"version": "7.1.1",
1665
+
"resolved": "https://registry.npmjs.org/ansi-escapes/-/ansi-escapes-7.1.1.tgz",
1666
+
"integrity": "sha512-Zhl0ErHcSRUaVfGUeUdDuLgpkEo8KIFjB4Y9uAc46ScOpdDiU1Dbyplh7qWJeJ/ZHpbyMSM26+X3BySgnIz40Q==",
1667
+
"dev": true,
1668
+
"license": "MIT",
1669
+
"dependencies": {
1670
+
"environment": "^1.0.0"
1671
+
},
1672
+
"engines": {
1673
+
"node": ">=18"
1674
+
},
1675
+
"funding": {
1676
+
"url": "https://github.com/sponsors/sindresorhus"
1677
+
}
1678
+
},
1679
+
"node_modules/ansi-regex": {
1680
+
"version": "6.2.2",
1681
+
"resolved": "https://registry.npmjs.org/ansi-regex/-/ansi-regex-6.2.2.tgz",
1682
+
"integrity": "sha512-Bq3SmSpyFHaWjPk8If9yc6svM8c56dB5BAtW4Qbw5jHTwwXXcTLoRMkpDJp6VL0XzlWaCHTXrkFURMYmD0sLqg==",
1683
+
"dev": true,
1684
+
"license": "MIT",
1685
+
"engines": {
1686
+
"node": ">=12"
1687
+
},
1688
+
"funding": {
1689
+
"url": "https://github.com/chalk/ansi-regex?sponsor=1"
1690
+
}
1691
+
},
1661
1692
"node_modules/ansi-styles": {
1662
1693
"version": "4.3.0",
1663
1694
"resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz",
···
1811
1842
"node": ">= 6"
1812
1843
}
1813
1844
},
1845
+
"node_modules/cli-cursor": {
1846
+
"version": "5.0.0",
1847
+
"resolved": "https://registry.npmjs.org/cli-cursor/-/cli-cursor-5.0.0.tgz",
1848
+
"integrity": "sha512-aCj4O5wKyszjMmDT4tZj93kxyydN/K5zPWSCe6/0AV/AA1pqe5ZBIw0a2ZfPQV7lL5/yb5HsUreJ6UFAF1tEQw==",
1849
+
"dev": true,
1850
+
"license": "MIT",
1851
+
"dependencies": {
1852
+
"restore-cursor": "^5.0.0"
1853
+
},
1854
+
"engines": {
1855
+
"node": ">=18"
1856
+
},
1857
+
"funding": {
1858
+
"url": "https://github.com/sponsors/sindresorhus"
1859
+
}
1860
+
},
1861
+
"node_modules/cli-truncate": {
1862
+
"version": "5.1.0",
1863
+
"resolved": "https://registry.npmjs.org/cli-truncate/-/cli-truncate-5.1.0.tgz",
1864
+
"integrity": "sha512-7JDGG+4Zp0CsknDCedl0DYdaeOhc46QNpXi3NLQblkZpXXgA6LncLDUUyvrjSvZeF3VRQa+KiMGomazQrC1V8g==",
1865
+
"dev": true,
1866
+
"license": "MIT",
1867
+
"dependencies": {
1868
+
"slice-ansi": "^7.1.0",
1869
+
"string-width": "^8.0.0"
1870
+
},
1871
+
"engines": {
1872
+
"node": ">=20"
1873
+
},
1874
+
"funding": {
1875
+
"url": "https://github.com/sponsors/sindresorhus"
1876
+
}
1877
+
},
1814
1878
"node_modules/color-convert": {
1815
1879
"version": "2.0.1",
1816
1880
"resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz",
···
1837
1901
"integrity": "sha512-IfEDxwoWIjkeXL1eXcDiow4UbKjhLdq6/EuSVR9GMN7KVH3r9gQ83e73hsz1Nd1T3ijd5xv1wcWRYO+D6kCI2w==",
1838
1902
"dev": true,
1839
1903
"license": "MIT"
1904
+
},
1905
+
"node_modules/commander": {
1906
+
"version": "14.0.1",
1907
+
"resolved": "https://registry.npmjs.org/commander/-/commander-14.0.1.tgz",
1908
+
"integrity": "sha512-2JkV3gUZUVrbNA+1sjBOYLsMZ5cEEl8GTFP2a4AVz5hvasAMCQ1D2l2le/cX+pV4N6ZU17zjUahLpIXRrnWL8A==",
1909
+
"dev": true,
1910
+
"license": "MIT",
1911
+
"engines": {
1912
+
"node": ">=20"
1913
+
}
1840
1914
},
1841
1915
"node_modules/concat-map": {
1842
1916
"version": "0.0.1",
···
1902
1976
"node": ">=0.3.1"
1903
1977
}
1904
1978
},
1979
+
"node_modules/emoji-regex": {
1980
+
"version": "10.5.0",
1981
+
"resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-10.5.0.tgz",
1982
+
"integrity": "sha512-lb49vf1Xzfx080OKA0o6l8DQQpV+6Vg95zyCJX9VB/BqKYlhG7N4wgROUUHRA+ZPUefLnteQOad7z1kT2bV7bg==",
1983
+
"dev": true,
1984
+
"license": "MIT"
1985
+
},
1986
+
"node_modules/environment": {
1987
+
"version": "1.1.0",
1988
+
"resolved": "https://registry.npmjs.org/environment/-/environment-1.1.0.tgz",
1989
+
"integrity": "sha512-xUtoPkMggbz0MPyPiIWr1Kp4aeWJjDZ6SMvURhimjdZgsRuDplF5/s9hcgGhyXMhs+6vpnuoiZ2kFiu3FMnS8Q==",
1990
+
"dev": true,
1991
+
"license": "MIT",
1992
+
"engines": {
1993
+
"node": ">=18"
1994
+
},
1995
+
"funding": {
1996
+
"url": "https://github.com/sponsors/sindresorhus"
1997
+
}
1998
+
},
1905
1999
"node_modules/esbuild": {
1906
2000
"version": "0.25.5",
1907
2001
"resolved": "https://registry.npmjs.org/esbuild/-/esbuild-0.25.5.tgz",
···
2134
2228
"node": ">=0.10.0"
2135
2229
}
2136
2230
},
2231
+
"node_modules/eventemitter3": {
2232
+
"version": "5.0.1",
2233
+
"resolved": "https://registry.npmjs.org/eventemitter3/-/eventemitter3-5.0.1.tgz",
2234
+
"integrity": "sha512-GWkBvjiSZK87ELrYOSESUYeVIc9mvLLf/nXalMOS5dYrgZq9o5OVkbZAVM06CVxYsCwH9BDZFPlQTlPA1j4ahA==",
2235
+
"dev": true,
2236
+
"license": "MIT"
2237
+
},
2137
2238
"node_modules/fast-deep-equal": {
2138
2239
"version": "3.1.3",
2139
2240
"resolved": "https://registry.npmjs.org/fast-deep-equal/-/fast-deep-equal-3.1.3.tgz",
···
2274
2375
"node": "^8.16.0 || ^10.6.0 || >=11.0.0"
2275
2376
}
2276
2377
},
2378
+
"node_modules/get-east-asian-width": {
2379
+
"version": "1.4.0",
2380
+
"resolved": "https://registry.npmjs.org/get-east-asian-width/-/get-east-asian-width-1.4.0.tgz",
2381
+
"integrity": "sha512-QZjmEOC+IT1uk6Rx0sX22V6uHWVwbdbxf1faPqJ1QhLdGgsRGCZoyaQBm/piRdJy/D2um6hM1UP7ZEeQ4EkP+Q==",
2382
+
"dev": true,
2383
+
"license": "MIT",
2384
+
"engines": {
2385
+
"node": ">=18"
2386
+
},
2387
+
"funding": {
2388
+
"url": "https://github.com/sponsors/sindresorhus"
2389
+
}
2390
+
},
2277
2391
"node_modules/glob-parent": {
2278
2392
"version": "6.0.2",
2279
2393
"resolved": "https://registry.npmjs.org/glob-parent/-/glob-parent-6.0.2.tgz",
···
2348
2462
"node": ">=8"
2349
2463
}
2350
2464
},
2465
+
"node_modules/husky": {
2466
+
"version": "9.1.7",
2467
+
"resolved": "https://registry.npmjs.org/husky/-/husky-9.1.7.tgz",
2468
+
"integrity": "sha512-5gs5ytaNjBrh5Ow3zrvdUUY+0VxIuWVL4i9irt6friV+BqdCfmV11CQTWMiBYWHbXhco+J1kHfTOUkePhCDvMA==",
2469
+
"dev": true,
2470
+
"license": "MIT",
2471
+
"bin": {
2472
+
"husky": "bin.js"
2473
+
},
2474
+
"engines": {
2475
+
"node": ">=18"
2476
+
},
2477
+
"funding": {
2478
+
"url": "https://github.com/sponsors/typicode"
2479
+
}
2480
+
},
2351
2481
"node_modules/ignore": {
2352
2482
"version": "5.3.2",
2353
2483
"resolved": "https://registry.npmjs.org/ignore/-/ignore-5.3.2.tgz",
···
2408
2538
"node": ">=0.10.0"
2409
2539
}
2410
2540
},
2541
+
"node_modules/is-fullwidth-code-point": {
2542
+
"version": "5.1.0",
2543
+
"resolved": "https://registry.npmjs.org/is-fullwidth-code-point/-/is-fullwidth-code-point-5.1.0.tgz",
2544
+
"integrity": "sha512-5XHYaSyiqADb4RnZ1Bdad6cPp8Toise4TzEjcOYDHZkTCbKgiUl7WTUCpNWHuxmDt91wnsZBc9xinNzopv3JMQ==",
2545
+
"dev": true,
2546
+
"license": "MIT",
2547
+
"dependencies": {
2548
+
"get-east-asian-width": "^1.3.1"
2549
+
},
2550
+
"engines": {
2551
+
"node": ">=18"
2552
+
},
2553
+
"funding": {
2554
+
"url": "https://github.com/sponsors/sindresorhus"
2555
+
}
2556
+
},
2411
2557
"node_modules/is-glob": {
2412
2558
"version": "4.0.3",
2413
2559
"resolved": "https://registry.npmjs.org/is-glob/-/is-glob-4.0.3.tgz",
···
2496
2642
"node": ">= 0.8.0"
2497
2643
}
2498
2644
},
2645
+
"node_modules/lint-staged": {
2646
+
"version": "16.2.3",
2647
+
"resolved": "https://registry.npmjs.org/lint-staged/-/lint-staged-16.2.3.tgz",
2648
+
"integrity": "sha512-1OnJEESB9zZqsp61XHH2fvpS1es3hRCxMplF/AJUDa8Ho8VrscYDIuxGrj3m8KPXbcWZ8fT9XTMUhEQmOVKpKw==",
2649
+
"dev": true,
2650
+
"license": "MIT",
2651
+
"dependencies": {
2652
+
"commander": "^14.0.1",
2653
+
"listr2": "^9.0.4",
2654
+
"micromatch": "^4.0.8",
2655
+
"nano-spawn": "^1.0.3",
2656
+
"pidtree": "^0.6.0",
2657
+
"string-argv": "^0.3.2",
2658
+
"yaml": "^2.8.1"
2659
+
},
2660
+
"bin": {
2661
+
"lint-staged": "bin/lint-staged.js"
2662
+
},
2663
+
"engines": {
2664
+
"node": ">=20.17"
2665
+
},
2666
+
"funding": {
2667
+
"url": "https://opencollective.com/lint-staged"
2668
+
}
2669
+
},
2670
+
"node_modules/listr2": {
2671
+
"version": "9.0.4",
2672
+
"resolved": "https://registry.npmjs.org/listr2/-/listr2-9.0.4.tgz",
2673
+
"integrity": "sha512-1wd/kpAdKRLwv7/3OKC8zZ5U8e/fajCfWMxacUvB79S5nLrYGPtUI/8chMQhn3LQjsRVErTb9i1ECAwW0ZIHnQ==",
2674
+
"dev": true,
2675
+
"license": "MIT",
2676
+
"dependencies": {
2677
+
"cli-truncate": "^5.0.0",
2678
+
"colorette": "^2.0.20",
2679
+
"eventemitter3": "^5.0.1",
2680
+
"log-update": "^6.1.0",
2681
+
"rfdc": "^1.4.1",
2682
+
"wrap-ansi": "^9.0.0"
2683
+
},
2684
+
"engines": {
2685
+
"node": ">=20.0.0"
2686
+
}
2687
+
},
2499
2688
"node_modules/locate-path": {
2500
2689
"version": "6.0.0",
2501
2690
"resolved": "https://registry.npmjs.org/locate-path/-/locate-path-6.0.0.tgz",
···
2519
2708
"dev": true,
2520
2709
"license": "MIT"
2521
2710
},
2711
+
"node_modules/log-update": {
2712
+
"version": "6.1.0",
2713
+
"resolved": "https://registry.npmjs.org/log-update/-/log-update-6.1.0.tgz",
2714
+
"integrity": "sha512-9ie8ItPR6tjY5uYJh8K/Zrv/RMZ5VOlOWvtZdEHYSTFKZfIBPQa9tOAEeAWhd+AnIneLJ22w5fjOYtoutpWq5w==",
2715
+
"dev": true,
2716
+
"license": "MIT",
2717
+
"dependencies": {
2718
+
"ansi-escapes": "^7.0.0",
2719
+
"cli-cursor": "^5.0.0",
2720
+
"slice-ansi": "^7.1.0",
2721
+
"strip-ansi": "^7.1.0",
2722
+
"wrap-ansi": "^9.0.0"
2723
+
},
2724
+
"engines": {
2725
+
"node": ">=18"
2726
+
},
2727
+
"funding": {
2728
+
"url": "https://github.com/sponsors/sindresorhus"
2729
+
}
2730
+
},
2522
2731
"node_modules/merge2": {
2523
2732
"version": "1.4.1",
2524
2733
"resolved": "https://registry.npmjs.org/merge2/-/merge2-1.4.1.tgz",
···
2543
2752
"node": ">=8.6"
2544
2753
}
2545
2754
},
2755
+
"node_modules/mimic-function": {
2756
+
"version": "5.0.1",
2757
+
"resolved": "https://registry.npmjs.org/mimic-function/-/mimic-function-5.0.1.tgz",
2758
+
"integrity": "sha512-VP79XUPxV2CigYP3jWwAUFSku2aKqBH7uTAapFWCBqutsbmDo96KY5o8uh6U+/YSIn5OxJnXp73beVkpqMIGhA==",
2759
+
"dev": true,
2760
+
"license": "MIT",
2761
+
"engines": {
2762
+
"node": ">=18"
2763
+
},
2764
+
"funding": {
2765
+
"url": "https://github.com/sponsors/sindresorhus"
2766
+
}
2767
+
},
2546
2768
"node_modules/minimatch": {
2547
2769
"version": "3.1.2",
2548
2770
"resolved": "https://registry.npmjs.org/minimatch/-/minimatch-3.1.2.tgz",
···
2562
2784
"integrity": "sha512-6FlzubTLZG3J2a/NVCAleEhjzq5oxgHyaCU9yYXvcLsvoVaHJq/s5xXI6/XXP6tz7R9xAOtHnSO/tXtF3WRTlA==",
2563
2785
"dev": true,
2564
2786
"license": "MIT"
2787
+
},
2788
+
"node_modules/nano-spawn": {
2789
+
"version": "1.0.3",
2790
+
"resolved": "https://registry.npmjs.org/nano-spawn/-/nano-spawn-1.0.3.tgz",
2791
+
"integrity": "sha512-jtpsQDetTnvS2Ts1fiRdci5rx0VYws5jGyC+4IYOTnIQ/wwdf6JdomlHBwqC3bJYOvaKu0C2GSZ1A60anrYpaA==",
2792
+
"dev": true,
2793
+
"license": "MIT",
2794
+
"engines": {
2795
+
"node": ">=20.17"
2796
+
},
2797
+
"funding": {
2798
+
"url": "https://github.com/sindresorhus/nano-spawn?sponsor=1"
2799
+
}
2565
2800
},
2566
2801
"node_modules/nanoid": {
2567
2802
"version": "3.3.11",
···
2618
2853
"onchange": "dist/bin.js"
2619
2854
}
2620
2855
},
2856
+
"node_modules/onetime": {
2857
+
"version": "7.0.0",
2858
+
"resolved": "https://registry.npmjs.org/onetime/-/onetime-7.0.0.tgz",
2859
+
"integrity": "sha512-VXJjc87FScF88uafS3JllDgvAm+c/Slfz06lorj2uAY34rlUu0Nt+v8wreiImcrgAjjIHp1rXpTDlLOGw29WwQ==",
2860
+
"dev": true,
2861
+
"license": "MIT",
2862
+
"dependencies": {
2863
+
"mimic-function": "^5.0.0"
2864
+
},
2865
+
"engines": {
2866
+
"node": ">=18"
2867
+
},
2868
+
"funding": {
2869
+
"url": "https://github.com/sponsors/sindresorhus"
2870
+
}
2871
+
},
2621
2872
"node_modules/optionator": {
2622
2873
"version": "0.9.4",
2623
2874
"resolved": "https://registry.npmjs.org/optionator/-/optionator-0.9.4.tgz",
···
2732
2983
},
2733
2984
"funding": {
2734
2985
"url": "https://github.com/sponsors/jonschlinkert"
2986
+
}
2987
+
},
2988
+
"node_modules/pidtree": {
2989
+
"version": "0.6.0",
2990
+
"resolved": "https://registry.npmjs.org/pidtree/-/pidtree-0.6.0.tgz",
2991
+
"integrity": "sha512-eG2dWTVw5bzqGRztnHExczNxt5VGsE6OwTeCG3fdUf9KBsZzO3R5OIIIzWR+iZA0NtZ+RDVdaoE2dK1cn6jH4g==",
2992
+
"dev": true,
2993
+
"license": "MIT",
2994
+
"bin": {
2995
+
"pidtree": "bin/pidtree.js"
2996
+
},
2997
+
"engines": {
2998
+
"node": ">=0.10"
2735
2999
}
2736
3000
},
2737
3001
"node_modules/postcss": {
···
2888
3152
"node": ">=4"
2889
3153
}
2890
3154
},
3155
+
"node_modules/restore-cursor": {
3156
+
"version": "5.1.0",
3157
+
"resolved": "https://registry.npmjs.org/restore-cursor/-/restore-cursor-5.1.0.tgz",
3158
+
"integrity": "sha512-oMA2dcrw6u0YfxJQXm342bFKX/E4sG9rbTzO9ptUcR/e8A33cHuvStiYOwH7fszkZlZ1z/ta9AAoPk2F4qIOHA==",
3159
+
"dev": true,
3160
+
"license": "MIT",
3161
+
"dependencies": {
3162
+
"onetime": "^7.0.0",
3163
+
"signal-exit": "^4.1.0"
3164
+
},
3165
+
"engines": {
3166
+
"node": ">=18"
3167
+
},
3168
+
"funding": {
3169
+
"url": "https://github.com/sponsors/sindresorhus"
3170
+
}
3171
+
},
2891
3172
"node_modules/reusify": {
2892
3173
"version": "1.1.0",
2893
3174
"resolved": "https://registry.npmjs.org/reusify/-/reusify-1.1.0.tgz",
···
2898
3179
"iojs": ">=1.0.0",
2899
3180
"node": ">=0.10.0"
2900
3181
}
3182
+
},
3183
+
"node_modules/rfdc": {
3184
+
"version": "1.4.1",
3185
+
"resolved": "https://registry.npmjs.org/rfdc/-/rfdc-1.4.1.tgz",
3186
+
"integrity": "sha512-q1b3N5QkRUWUl7iyylaaj3kOpIT0N2i9MqIEQXP73GVsN9cw3fdx8X63cEmWhJGi2PPCF23Ijp7ktmd39rawIA==",
3187
+
"dev": true,
3188
+
"license": "MIT"
2901
3189
},
2902
3190
"node_modules/rollup": {
2903
3191
"version": "4.43.0",
···
3012
3300
"node": ">=8"
3013
3301
}
3014
3302
},
3303
+
"node_modules/signal-exit": {
3304
+
"version": "4.1.0",
3305
+
"resolved": "https://registry.npmjs.org/signal-exit/-/signal-exit-4.1.0.tgz",
3306
+
"integrity": "sha512-bzyZ1e88w9O1iNJbKnOlvYTrWPDl46O1bG0D3XInv+9tkPrxrN8jUUTiFlDkkmKWgn1M6CfIA13SuGqOa9Korw==",
3307
+
"dev": true,
3308
+
"license": "ISC",
3309
+
"engines": {
3310
+
"node": ">=14"
3311
+
},
3312
+
"funding": {
3313
+
"url": "https://github.com/sponsors/isaacs"
3314
+
}
3315
+
},
3015
3316
"node_modules/slash": {
3016
3317
"version": "5.1.0",
3017
3318
"resolved": "https://registry.npmjs.org/slash/-/slash-5.1.0.tgz",
···
3025
3326
"url": "https://github.com/sponsors/sindresorhus"
3026
3327
}
3027
3328
},
3329
+
"node_modules/slice-ansi": {
3330
+
"version": "7.1.2",
3331
+
"resolved": "https://registry.npmjs.org/slice-ansi/-/slice-ansi-7.1.2.tgz",
3332
+
"integrity": "sha512-iOBWFgUX7caIZiuutICxVgX1SdxwAVFFKwt1EvMYYec/NWO5meOJ6K5uQxhrYBdQJne4KxiqZc+KptFOWFSI9w==",
3333
+
"dev": true,
3334
+
"license": "MIT",
3335
+
"dependencies": {
3336
+
"ansi-styles": "^6.2.1",
3337
+
"is-fullwidth-code-point": "^5.0.0"
3338
+
},
3339
+
"engines": {
3340
+
"node": ">=18"
3341
+
},
3342
+
"funding": {
3343
+
"url": "https://github.com/chalk/slice-ansi?sponsor=1"
3344
+
}
3345
+
},
3346
+
"node_modules/slice-ansi/node_modules/ansi-styles": {
3347
+
"version": "6.2.3",
3348
+
"resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-6.2.3.tgz",
3349
+
"integrity": "sha512-4Dj6M28JB+oAH8kFkTLUo+a2jwOFkuqb3yucU0CANcRRUbxS0cP0nZYCGjcc3BNXwRIsUVmDGgzawme7zvJHvg==",
3350
+
"dev": true,
3351
+
"license": "MIT",
3352
+
"engines": {
3353
+
"node": ">=12"
3354
+
},
3355
+
"funding": {
3356
+
"url": "https://github.com/chalk/ansi-styles?sponsor=1"
3357
+
}
3358
+
},
3028
3359
"node_modules/source-map-js": {
3029
3360
"version": "1.2.1",
3030
3361
"resolved": "https://registry.npmjs.org/source-map-js/-/source-map-js-1.2.1.tgz",
···
3035
3366
"node": ">=0.10.0"
3036
3367
}
3037
3368
},
3369
+
"node_modules/string-argv": {
3370
+
"version": "0.3.2",
3371
+
"resolved": "https://registry.npmjs.org/string-argv/-/string-argv-0.3.2.tgz",
3372
+
"integrity": "sha512-aqD2Q0144Z+/RqG52NeHEkZauTAUWJO8c6yTftGJKO3Tja5tUgIfmIl6kExvhtxSDP7fXB6DvzkfMpCd/F3G+Q==",
3373
+
"dev": true,
3374
+
"license": "MIT",
3375
+
"engines": {
3376
+
"node": ">=0.6.19"
3377
+
}
3378
+
},
3379
+
"node_modules/string-width": {
3380
+
"version": "8.1.0",
3381
+
"resolved": "https://registry.npmjs.org/string-width/-/string-width-8.1.0.tgz",
3382
+
"integrity": "sha512-Kxl3KJGb/gxkaUMOjRsQ8IrXiGW75O4E3RPjFIINOVH8AMl2SQ/yWdTzWwF3FevIX9LcMAjJW+GRwAlAbTSXdg==",
3383
+
"dev": true,
3384
+
"license": "MIT",
3385
+
"dependencies": {
3386
+
"get-east-asian-width": "^1.3.0",
3387
+
"strip-ansi": "^7.1.0"
3388
+
},
3389
+
"engines": {
3390
+
"node": ">=20"
3391
+
},
3392
+
"funding": {
3393
+
"url": "https://github.com/sponsors/sindresorhus"
3394
+
}
3395
+
},
3396
+
"node_modules/strip-ansi": {
3397
+
"version": "7.1.2",
3398
+
"resolved": "https://registry.npmjs.org/strip-ansi/-/strip-ansi-7.1.2.tgz",
3399
+
"integrity": "sha512-gmBGslpoQJtgnMAvOVqGZpEz9dyoKTCzy2nfz/n8aIFhN/jCE/rCmcxabB6jOOHV+0WNnylOxaxBQPSvcWklhA==",
3400
+
"dev": true,
3401
+
"license": "MIT",
3402
+
"dependencies": {
3403
+
"ansi-regex": "^6.0.1"
3404
+
},
3405
+
"engines": {
3406
+
"node": ">=12"
3407
+
},
3408
+
"funding": {
3409
+
"url": "https://github.com/chalk/strip-ansi?sponsor=1"
3410
+
}
3411
+
},
3038
3412
"node_modules/strip-json-comments": {
3039
3413
"version": "3.1.1",
3040
3414
"resolved": "https://registry.npmjs.org/strip-json-comments/-/strip-json-comments-3.1.1.tgz",
···
3216
3590
}
3217
3591
},
3218
3592
"node_modules/vite": {
3219
-
"version": "6.3.5",
3220
-
"resolved": "https://registry.npmjs.org/vite/-/vite-6.3.5.tgz",
3221
-
"integrity": "sha512-cZn6NDFE7wdTpINgs++ZJ4N49W2vRp8LCKrn3Ob1kYNtOo21vfDoaV5GzBfLU4MovSAB8uNRm4jgzVQZ+mBzPQ==",
3593
+
"version": "6.3.6",
3594
+
"resolved": "https://registry.npmjs.org/vite/-/vite-6.3.6.tgz",
3595
+
"integrity": "sha512-0msEVHJEScQbhkbVTb/4iHZdJ6SXp/AvxL2sjwYQFfBqleHtnCqv1J3sa9zbWz/6kW1m9Tfzn92vW+kZ1WV6QA==",
3222
3596
"dev": true,
3223
3597
"license": "MIT",
3224
3598
"dependencies": {
···
3342
3716
"license": "MIT",
3343
3717
"engines": {
3344
3718
"node": ">=0.10.0"
3719
+
}
3720
+
},
3721
+
"node_modules/wrap-ansi": {
3722
+
"version": "9.0.2",
3723
+
"resolved": "https://registry.npmjs.org/wrap-ansi/-/wrap-ansi-9.0.2.tgz",
3724
+
"integrity": "sha512-42AtmgqjV+X1VpdOfyTGOYRi0/zsoLqtXQckTmqTeybT+BDIbM/Guxo7x3pE2vtpr1ok6xRqM9OpBe+Jyoqyww==",
3725
+
"dev": true,
3726
+
"license": "MIT",
3727
+
"dependencies": {
3728
+
"ansi-styles": "^6.2.1",
3729
+
"string-width": "^7.0.0",
3730
+
"strip-ansi": "^7.1.0"
3731
+
},
3732
+
"engines": {
3733
+
"node": ">=18"
3734
+
},
3735
+
"funding": {
3736
+
"url": "https://github.com/chalk/wrap-ansi?sponsor=1"
3737
+
}
3738
+
},
3739
+
"node_modules/wrap-ansi/node_modules/ansi-styles": {
3740
+
"version": "6.2.3",
3741
+
"resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-6.2.3.tgz",
3742
+
"integrity": "sha512-4Dj6M28JB+oAH8kFkTLUo+a2jwOFkuqb3yucU0CANcRRUbxS0cP0nZYCGjcc3BNXwRIsUVmDGgzawme7zvJHvg==",
3743
+
"dev": true,
3744
+
"license": "MIT",
3745
+
"engines": {
3746
+
"node": ">=12"
3747
+
},
3748
+
"funding": {
3749
+
"url": "https://github.com/chalk/ansi-styles?sponsor=1"
3750
+
}
3751
+
},
3752
+
"node_modules/wrap-ansi/node_modules/string-width": {
3753
+
"version": "7.2.0",
3754
+
"resolved": "https://registry.npmjs.org/string-width/-/string-width-7.2.0.tgz",
3755
+
"integrity": "sha512-tsaTIkKW9b4N+AEj+SVA+WhJzV7/zMhcSu78mLKWSk7cXMOSHsBKFWUs0fWwq8QyK3MgJBQRX6Gbi4kYbdvGkQ==",
3756
+
"dev": true,
3757
+
"license": "MIT",
3758
+
"dependencies": {
3759
+
"emoji-regex": "^10.3.0",
3760
+
"get-east-asian-width": "^1.0.0",
3761
+
"strip-ansi": "^7.1.0"
3762
+
},
3763
+
"engines": {
3764
+
"node": ">=18"
3765
+
},
3766
+
"funding": {
3767
+
"url": "https://github.com/sponsors/sindresorhus"
3768
+
}
3769
+
},
3770
+
"node_modules/yaml": {
3771
+
"version": "2.8.1",
3772
+
"resolved": "https://registry.npmjs.org/yaml/-/yaml-2.8.1.tgz",
3773
+
"integrity": "sha512-lcYcMxX2PO9XMGvAJkJ3OsNMw+/7FKes7/hgerGUYWIoWu5j/+YQqcZr5JnPZWzOsEBgMbSbiSTn/dv/69Mkpw==",
3774
+
"dev": true,
3775
+
"license": "ISC",
3776
+
"bin": {
3777
+
"yaml": "bin.mjs"
3778
+
},
3779
+
"engines": {
3780
+
"node": ">= 14.6"
3345
3781
}
3346
3782
},
3347
3783
"node_modules/yocto-queue": {
+2
src/HOTerm.resi
+2
src/HOTerm.resi
+241
src/InductiveSet.res
+241
src/InductiveSet.res
···
1
+
open Signatures
2
+
open Component
3
+
open Util
4
+
5
+
// InductiveSet is specific to HOTerm to allow pattern matching on term structure
6
+
module Make = (
7
+
Term: TERM with type t = HOTerm.t and type meta = string,
8
+
Judgment: JUDGMENT with module Term := Term and type t = HOTerm.t,
9
+
JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
10
+
) => {
11
+
module Rule = Rule.Make(Term, Judgment)
12
+
module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
13
+
module Ports = Ports(Term, Judgment)
14
+
type state = dict<Rule.t>
15
+
type props = {
16
+
content: state,
17
+
imports: Ports.t,
18
+
onChange: (state, ~exports: Ports.t=?) => unit,
19
+
}
20
+
21
+
type constructorGroup = {
22
+
name: string,
23
+
arity: int,
24
+
rules: array<(string, Rule.t)>,
25
+
}
26
+
27
+
let makeKey = (name, arity) => name ++ "§" ++ Int.toString(arity)
28
+
29
+
let extractConstructorSignature = (rule: Rule.t): option<(string, int)> => {
30
+
let (head, args) = HOTerm.strip(rule.conclusion)
31
+
switch head {
32
+
| Symbol({name}) => Some((name, Array.length(args)))
33
+
| _ => None
34
+
}
35
+
}
36
+
37
+
let groupByConstructor = (rules: dict<Rule.t>): array<constructorGroup> =>
38
+
rules
39
+
->Dict.toArray
40
+
->Array.filterMap(((name, rule)) =>
41
+
extractConstructorSignature(rule)->Option.map(sig => (name, rule, sig))
42
+
)
43
+
->Array.reduce(Dict.make(), (acc, (name, rule, (cname, arity))) => {
44
+
let key = makeKey(cname, arity)
45
+
Dict.set(acc, key, [(name, rule), ...Dict.get(acc, key)->Option.getOr([])])
46
+
acc
47
+
})
48
+
->Dict.valuesToArray
49
+
->Array.map(constructors => {
50
+
let (_, firstRule) = constructors[0]->Option.getExn
51
+
let (name, arity) = extractConstructorSignature(firstRule)->Option.getExn
52
+
{name, arity, rules: constructors}
53
+
})
54
+
let generateInductionRule = (
55
+
group: constructorGroup,
56
+
allGroups: array<constructorGroup>,
57
+
): Rule.t => {
58
+
let {name: str, arity: i} = group
59
+
let numFormers = Array.length(allGroups)
60
+
let groupIndex = mustFindIndex(allGroups, g => g.name == str && g.arity == i)
61
+
62
+
let findFormerIndex = (name, arity) =>
63
+
mustFindIndex(allGroups, g => g.name == name && g.arity == arity)
64
+
65
+
let generateInductiveHypothesis = (premise: Rule.t, offset: int): option<Rule.t> => {
66
+
let (head, args) = HOTerm.strip(premise.conclusion)
67
+
switch head {
68
+
| Symbol({name}) =>
69
+
let formerIndex = findFormerIndex(name, Array.length(args))
70
+
Some({
71
+
Rule.vars: premise.vars,
72
+
premises: premise.premises,
73
+
conclusion: HOTerm.app(
74
+
HOTerm.Var({idx: offset + Array.length(premise.vars) + i + formerIndex}),
75
+
args,
76
+
),
77
+
})
78
+
| _ => None
79
+
}
80
+
}
81
+
82
+
let caseSubgoal = (constructorRule: Rule.t): Rule.t => {
83
+
let offset = Array.length(constructorRule.vars)
84
+
let inductiveHypotheses =
85
+
constructorRule.premises->Array.filterMap(premise =>
86
+
generateInductiveHypothesis(premise, offset)
87
+
)
88
+
89
+
let (conclusionHead, conclusionArgs) = HOTerm.strip(constructorRule.conclusion)
90
+
let typeIndex = switch conclusionHead {
91
+
| Symbol({name}) => findFormerIndex(name, Array.length(conclusionArgs))
92
+
| _ => raise(Unreachable("Constructor conclusion must have a Symbol head"))
93
+
}
94
+
95
+
{
96
+
Rule.vars: constructorRule.vars,
97
+
premises: Array.concat(constructorRule.premises, inductiveHypotheses),
98
+
conclusion: HOTerm.app(HOTerm.Var({idx: offset + i + typeIndex}), conclusionArgs),
99
+
}
100
+
}
101
+
102
+
let allConstructors = Array.flatMap(allGroups, g => g.rules)
103
+
let subgoals = Array.map(allConstructors, ((_, rule)) => caseSubgoal(rule))
104
+
105
+
{
106
+
Rule.vars: Array.concat(
107
+
Array.fromInitializer(~length=i, i => "§" ++ Int.toString(i)),
108
+
Array.fromInitializer(~length=numFormers, i => "§P" ++ Int.toString(i)),
109
+
),
110
+
premises: [
111
+
{
112
+
Rule.vars: [],
113
+
premises: [],
114
+
conclusion: HOTerm.app(HOTerm.Symbol({name: str}), HOTerm.mkvars(i)),
115
+
},
116
+
...subgoals,
117
+
],
118
+
conclusion: HOTerm.app(HOTerm.Var({idx: i + groupIndex}), HOTerm.mkvars(i)),
119
+
}
120
+
}
121
+
122
+
module StringCmp = Belt.Id.MakeComparable({
123
+
type t = string
124
+
let cmp = Pervasives.compare
125
+
})
126
+
127
+
let extractInductiveType = (premise: Rule.t): option<(string, int)> => {
128
+
let (head, args) = HOTerm.strip(premise.conclusion)
129
+
switch head {
130
+
| Symbol({name}) => Some((name, Array.length(args)))
131
+
| _ => None
132
+
}
133
+
}
134
+
135
+
let isSelfReference = (group: constructorGroup, (name, arity)): bool =>
136
+
name == group.name && arity == group.arity
137
+
138
+
let findDependencies = (group: constructorGroup): array<(string, int)> =>
139
+
group.rules
140
+
->Array.flatMap(((_name, rule)) => rule.premises->Array.filterMap(extractInductiveType))
141
+
->Array.filter(dep => !isSelfReference(group, dep))
142
+
143
+
let rec collectReachable = (
144
+
toVisit: array<(string, int)>,
145
+
visited: Belt.Set.t<string, StringCmp.identity>,
146
+
allGroups: array<constructorGroup>,
147
+
): Belt.Set.t<string, StringCmp.identity> =>
148
+
switch toVisit {
149
+
| [] => visited
150
+
| _ =>
151
+
let (name, arity) = toVisit[0]->Option.getExn
152
+
let rest = Array.sliceToEnd(toVisit, ~start=1)
153
+
let key = makeKey(name, arity)
154
+
155
+
if Belt.Set.has(visited, key) {
156
+
collectReachable(rest, visited, allGroups)
157
+
} else {
158
+
let visited = Belt.Set.add(visited, key)
159
+
let newDeps =
160
+
allGroups
161
+
->Array.find(g => g.name == name && g.arity == arity)
162
+
->Option.map(findDependencies)
163
+
->Option.getOr([])
164
+
collectReachable(Array.concat(rest, newDeps), visited, allGroups)
165
+
}
166
+
}
167
+
168
+
let findMutuallyInductiveComponent = (
169
+
targetGroup: constructorGroup,
170
+
allGroups: array<constructorGroup>,
171
+
): array<constructorGroup> => {
172
+
let reachableKeys = collectReachable(
173
+
[(targetGroup.name, targetGroup.arity)],
174
+
Belt.Set.make(~id=module(StringCmp)),
175
+
allGroups,
176
+
)
177
+
allGroups->Array.filter(g => Belt.Set.has(reachableKeys, makeKey(g.name, g.arity)))
178
+
}
179
+
180
+
let derived = (state: state): state =>
181
+
state
182
+
->groupByConstructor
183
+
->Array.map(group => {
184
+
let mutualComponent = findMutuallyInductiveComponent(group, groupByConstructor(state))
185
+
let rule = generateInductionRule(group, mutualComponent)
186
+
("§induction-" ++ makeKey(group.name, group.arity), rule)
187
+
})
188
+
->Dict.fromArray
189
+
let serialise = (state: state) =>
190
+
state
191
+
->Dict.toArray
192
+
->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k))
193
+
->Array.join("\n")
194
+
let deserialise = (str: string, ~imports as _: Ports.t) => {
195
+
let cur = ref(str)
196
+
let go = ref(true)
197
+
let results = Dict.make()
198
+
let ret = ref(Error("impossible"))
199
+
while go.contents {
200
+
switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
201
+
| Ok((t, n), rest) =>
202
+
if n->String.trim == "" {
203
+
go := false
204
+
ret := Error("Rule given with no name")
205
+
} else {
206
+
Dict.set(results, n, t)
207
+
if rest->String.trim == "" {
208
+
go := false
209
+
ret := Ok(results)
210
+
} else {
211
+
cur := rest
212
+
}
213
+
}
214
+
| Error(e) => {
215
+
go := false
216
+
ret := Error(e)
217
+
}
218
+
}
219
+
}
220
+
ret.contents->Result.map(state => (state, {Ports.facts: state, ruleStyle: None}))
221
+
}
222
+
223
+
let make = props => {
224
+
<div
225
+
className={"axiom-set axiom-set-"->String.concat(
226
+
String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
227
+
)}>
228
+
{Dict.toArray(props.content->Dict.copy->Dict.assign(derived(props.content)))
229
+
->Array.mapWithIndex(((n, r), i) =>
230
+
<RuleView
231
+
rule={r}
232
+
scope={[]}
233
+
key={String.make(i)}
234
+
style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
235
+
{React.string(n)}
236
+
</RuleView>
237
+
)
238
+
->React.array}
239
+
</div>
240
+
}
241
+
}
+1
src/Scratch.res
+1
src/Scratch.res
+6
src/Util.res
+6
src/Util.res
+2
-1
src/testcomponent.tsx
+2
-1
src/testcomponent.tsx
···
1
1
import * as ComponentGraph from './componentgraph'
2
-
import { AxiomS, ConfS, TheoremS } from './Scratch.mjs'
2
+
import { AxiomS, ConfS, TheoremS, InductiveS } from './Scratch.mjs'
3
3
import ReactDOM from 'react-dom/client';
4
4
import React from 'react';
5
5
···
76
76
window.localStorage.clear()
77
77
ComponentGraph.setup({
78
78
"hol-comp": HolComp(AxiomS),
79
+
"hol-inductive": HolComp(InductiveS),
79
80
"hol-config":HolComp(ConfS),
80
81
"hol-proof": HolComp(TheoremS)
81
82
});