lambdapi
lambdapi copied to clipboard
Deducteam
Proof assistant based on the λΠ-calculus modulo rewriting
In bulk: - In #671 @QGarchery suggests to allow rewriting on hypothesis. But we can imagine allowing the tatic "simplify" too. For now, it's possible by using the tactic "simplify"...
``` opaque symbol size_undup [a] (beq:τ a → τ a → 𝔹) (l:𝕃 a) : π (istrue (size (undup beq l) ≤ size l)) ≔ begin assume a beq; induction...
When we have things like `opaque symbol m n p : ...`, it may be useful in some case to do things like `induction p` instead of changing the definition...
``` opaque symbol leq_add2l p m n : π (istrue (p + m ≤ p + n) ⇔ istrue (m ≤ n)) ≔ begin assume p m n; apply ∧ᵢ...
``` symbol ! : ℕ → ℕ; notation ! postfix 40; rule 0 ! ↪ 1 with (s $n) ! ↪ (s $n) × $n !; opaque symbol fact0 :...
``` require open Blanqui.Lib.Set Blanqui.Lib.Prop Blanqui.Lib.Eq Blanqui.Lib.Bool; symbol istrue : 𝔹 → Prop; rule istrue true ↪ ⊤ with istrue false ↪ ⊥; symbol b : π(true ≠ false) ≔...
Comparison on 22/02/24 of db branch 60945055 with master branch 9597727 on Intel(R) Core(TM) i7-8665U CPU @ 1.90GHz with 32Go RAM and ocaml 4.14.1: | library | master | db...
TODO - [ ] remove --confluence/--termination options ? - [ ] check XTC output - [ ] add tests for HRS and XTC outputs
Add a skolemization tactic. **TODO:** - [ ] nnf and pnf transformations should generate proof terms - [ ] skolemization should be applied on some hypothesis, not on the goal...
The following LambdaPi code symbol cmd : TYPE; symbol value : TYPE; symbol union : cmd → cmd → cmd ; symbol bind : cmd → (value → cmd) →...
