2d52d44710
This PR modifies the generation of induction and partial correctness
lemmas for `mutual` blocks defined via `partial_fixpoint`. Additionally,
the generation of lattice-theoretic induction principles of functions
via `mutual` blocks is modified for consistency with `partial_fixpoint`.
The lemmas now come in two variants:
1. A conjunction variant that combines conclusions for all elements of
the mutual block. This is generated only for the first function inside
of the mutual block.
2. Projected variants for each function separately
## Example 1
```lean4
axiom A : Type
axiom B : Type
axiom A.toB : A → B
axiom B.toA : B → A
mutual
noncomputable def f : A := g.toA
partial_fixpoint
noncomputable def g : B := f.toB
partial_fixpoint
end
```
Generated `fixpoint_induct` lemmas:
```lean4
f.fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1)
(adm_2 : admissible motive_2) (h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA)
(h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) : motive_1 f
g.fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1)
(adm_2 : admissible motive_2) (h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA)
(h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) : motive_2 g
```
Mutual (conjunction) variant:
```lean4
f.mutual_fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1) (adm_2 : admissible motive_2)
(h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA) (h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) :
motive_1 f ∧ motive_2 g
```
## Example 2
```lean4
mutual
def f (n : Nat) : Option Nat :=
g (n + 1)
partial_fixpoint
def g (n : Nat) : Option Nat :=
if n = 0 then .none else f (n + 1)
partial_fixpoint
end
```
Generated `partial_correctness` lemmas (in a projected variant):
```lean4
f.partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
(h_1 :
∀ (g : Nat → Option Nat),
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
(h_2 :
∀ (f : Nat → Option Nat),
(∀ (n r : Nat), f n = some r → motive_1 n r) →
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r)
(n r✝ : Nat) : f n = some r✝ → motive_1 n r✝
g.partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
(h_1 :
∀ (g : Nat → Option Nat),
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
(h_2 :
∀ (f : Nat → Option Nat),
(∀ (n r : Nat), f n = some r → motive_1 n r) →
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r)
(n r✝ : Nat) : g n = some r✝ → motive_2 n r✝
```
Mutual (conjunction) variant:
```
f.mutual_partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
(h_1 :
∀ (g : Nat → Option Nat),
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
(h_2 :
∀ (f : Nat → Option Nat),
(∀ (n r : Nat), f n = some r → motive_1 n r) →
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r) :
(∀ (n r : Nat), f n = some r → motive_1 n r) ∧ ∀ (n r : Nat), g n = some r → motive_2 n r
```
57 lines
1.8 KiB
Text
57 lines
1.8 KiB
Text
axiom A : Type
|
||
axiom B : Type
|
||
|
||
axiom A.toB : A → B
|
||
axiom B.toA : B → A
|
||
|
||
open Lean.Order
|
||
|
||
instance : PartialOrder A := sorry
|
||
-- It’s important that the CCPO instance isn't completely axiomatic, so that
|
||
-- `instCCPO.toOrder` is defeq to `instOrder`
|
||
instance : CCPO A where
|
||
csup := sorry
|
||
csup_spec := sorry
|
||
instance : PartialOrder B := sorry
|
||
instance : CCPO B where
|
||
csup := sorry
|
||
csup_spec := sorry
|
||
|
||
@[partial_fixpoint_monotone] axiom monotone_toA :
|
||
∀ {α} [PartialOrder α] (f : α → B), monotone f → monotone (fun x => B.toA (f x))
|
||
@[partial_fixpoint_monotone] axiom monotone_toB :
|
||
∀ {α} [PartialOrder α] (f : α → A), monotone f → monotone (fun x => A.toB (f x))
|
||
|
||
mutual
|
||
noncomputable def f : A := g.toA
|
||
partial_fixpoint
|
||
noncomputable def g : B := f.toB
|
||
partial_fixpoint
|
||
end
|
||
|
||
/--
|
||
info: equations:
|
||
theorem f.eq_1 : f = g.toA
|
||
-/
|
||
#guard_msgs in #print equations f
|
||
/--
|
||
info: f.fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1)
|
||
(adm_2 : admissible motive_2) (h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA)
|
||
(h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) : motive_1 f
|
||
-/
|
||
#guard_msgs in
|
||
#check f.fixpoint_induct
|
||
/--
|
||
info: g.fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1)
|
||
(adm_2 : admissible motive_2) (h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA)
|
||
(h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) : motive_2 g
|
||
-/
|
||
#guard_msgs in
|
||
#check g.fixpoint_induct
|
||
/--
|
||
info: f.mutual_fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1)
|
||
(adm_2 : admissible motive_2) (h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA)
|
||
(h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) : motive_1 f ∧ motive_2 g
|
||
-/
|
||
#guard_msgs in
|
||
#check f.mutual_fixpoint_induct
|