Is this inductive type not well founded? How can I make it?

Stream: lean4

[Jared green]

I built a solver for circuits starting like this:

import Init.Data.List
open Classical
universe u

Inductive normalizable (a : Type u) [DecidableEq a] (pred : a -> Prop) where
  | atom : a -> (normalizable a pred)
  | And : List (normalizable a pred) -> normalizable a pred
  | Or : List (normalizable a pred) -> normalizable a pred
  | Not : normalizable a pred -> normalizable a pred

namespace normalizable

instance: DecidableEq (normalizable a pred) :=
  by
  sorry

def toProp (n : normalizable a pred) : Prop  :=
  match n with
  | atom a => pred a
  | And l => (l.map toProp).foldr \and true
  | Or l => (l.map toProp).foldr \or false
  | Not i => \neg(toProp i)

Apparently lean can’t tell toProp terminates.

[Tomas Skrivan]

Reimplementing List.map+List.foldr works and it is not too much more code

import Init.Data.List
open Classical
universe u

inductive normalizable (a : Type u) [DecidableEq a] (pred : a -> Prop) where
  | atom : a -> (normalizable a pred)
  | And : List (normalizable a pred) -> normalizable a pred
  | Or : List (normalizable a pred) -> normalizable a pred
  | Not : normalizable a pred -> normalizable a pred

namespace normalizable

instance: DecidableEq (normalizable a pred) :=
  by
  sorry

def toProp (n : normalizable a pred) : Prop  :=
  match n with
  | atom a => pred a
  | And [] => True
  | And (x::xs) => toProp x ∧ toProp (And xs)
  | Or [] => False
  | Or (x::xs) => toProp x ∨ toProp (Or xs)
  | Not i => ¬(toProp i)

Unfortunately I have very little experience with the termination checker so I don't know how to prove termination with map and fold

[Tomas Skrivan]

btw your code didn't compile. You can use the icon on the right top corner of the code block to open it in web editor to check if it compiles.

[Jared green]

Sorry, unfortunately I don’t know how to type in special symbols in zulip.

[Arthur Adjedj]

Using List.attach helps Lean understand that your function is well-founded:

import Init.Data.List
import Std.Data.List
open Classical
universe u

inductive normalizable (a : Type u) [DecidableEq a] (pred : a -> Prop) where
  | atom : a -> (normalizable a pred)
  | And : List (normalizable a pred) -> normalizable a pred
  | Or : List (normalizable a pred) -> normalizable a pred
  | Not : normalizable a pred -> normalizable a pred

namespace normalizable

instance: DecidableEq (normalizable a pred) :=
  by
  sorry

def toProp (n : normalizable a pred) : Prop  :=
  match n with
  | atom a => pred a
  | And l => (l.attach.map (fun ⟨x,_⟩ => toProp x)).foldr (· ∧ ·) True
  | Or l => (l.attach.map (fun ⟨x,_⟩ => toProp x)).foldr (· ∨ ·) False
  | Not i => ¬ toProp i

[Jared green]

the (x,_) gets a type mismatch. go with

fun x => x.val

and yet it still doesnt work, i still get the original problem.

[Jared green]

says

structural recursion cannot be used

[Jared green]

image.png

[Jared green]

version: 4.6.0-rc1

[Marcus Rossel]

import Std.Data.List
open Classical

inductive Normalizable (α : Type _) [DecidableEq α] (pred : α → Prop) where
  | atom : α → Normalizable α pred
  | and  : List (Normalizable α pred) → Normalizable α pred
  | or   : List (Normalizable α pred) → Normalizable α pred
  | not  : (Normalizable α pred) → Normalizable α pred

namespace Normalizable

instance : DecidableEq (Normalizable α pred) := by
  sorry

def toProp : Normalizable α pred → Prop
  | atom a => pred a
  | and l  => l.attach.map (toProp ·.val) |>.foldr (· ∧ ·) True
  | or l   => l.attach.map (toProp ·.val) |>.foldr (· ∨ ·) False
  | not i  => ¬(toProp i)
termination_by n => n
decreasing_by
  all_goals
    simp_wf
    try have := Subtype.property ‹_›
    decreasing_trivial

[Jared green]

image.png

[Marcus Rossel]

Yes, in your case line 38 should be termination_by n.

[Jared green]

image.png

[Timo Carlin-Burns]

Shouldn't it be termination_by sizeOf n?

[Ruben Van de Velde]

(deleted)

[Marcus Rossel]

Timo Carlin-Burns said:

Shouldn't it be termination_by sizeOf n?

With or without sizeOf works.

[Marcus Rossel]

@Jared green what does #eval Lean.versionString print out for you?

[Jared green]

"4.6.0-rc1"

[Marcus Rossel]

Then I'm very confused, as this exact code snippet works in the web editor:

import Init.Data.List
import Std.Data.List
open Classical
universe u

inductive normalizable (a : Type u) [DecidableEq a] (pred : a -> Prop) where
  | atom : a -> (normalizable a pred)
  | And : List (normalizable a pred) -> normalizable a pred
  | Or : List (normalizable a pred) -> normalizable a pred
  | Not : normalizable a pred -> normalizable a pred

namespace normalizable

instance: DecidableEq (normalizable a pred) :=
  by
  sorry

def toProp (n : normalizable a pred) : Prop  :=
  match n with
  | atom a => pred a
  | And l => (l.attach.map (fun x => toProp x.val)).foldr (· ∧ ·) True
  | Or l => (l.attach.map (fun x => toProp x.val)).foldr (· ∨ ·) False
  | Not i => ¬ toProp i
termination_by n
decreasing_by
  all_goals
    simp_wf
    try have := Subtype.property ‹_›
    decreasing_trivial

[Jared green]

image.png

[Jared green]

for context, this function turns each logic gate into a variable width truth table, which can accommodate implications.

[Arthur Adjedj]

Jared green said:

the (x,_) gets a type mismatch. go with

fun x => x.val

and yet it still doesnt work, i still get the original problem.

Your brackets are wrong. You need to write ⟨x,_⟩ (written as \< and \> respectively) instead of (x,_). Feel free to simply copy/paste the code written.

[Jared green]

next time.

[Kevin Buzzard]

One issue here @Jared green is that you keep posting screenshots (which are hard to read and debug) rather than posting code (which others can cut and paste) and cutting/pasting the code which other users are posting.

[Jared green]

its so the messages can be seen.

[Marcus Rossel]

Jared green said:

its so the messages can be seen.

I get the idea, but the messages aren't too helpful if we can't access the exact code that produced them. Please try constructing a #mwe in the future.

[Jared green]

got it

[Jared green]

the code so far:

import Init.Data.List
import Std.Data.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
open Classical

universe u

inductive normalizable (α : Type u) [DecidableEq α] (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : List (normalizable α pred) -> normalizable α pred
  | Or : List (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred

namespace normalizable

instance : DecidableEq (normalizable α pred) :=
  by
  intro a
  intro b


def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And l => (l.attach.map (fun x => toProp x.val)).foldr (· ∧ ·) True
  | Or l => (l.attach.map (fun x => toProp x.val)).foldr (· ∨ ·) False
  | Not n => ¬(toProp n)
termination_by n
  decreasing_by
  all_goals
    simp_wf
    try have := Subtype.property ‹_›
  decreasing_trivial
  simp_wf
  decreasing_trivial

def subnormalizeN (n : normalizable α pred) [DecidableEq (normalizable α pred)] : List (normalizable α pred) :=
  match n with
  | Or l => ((Or (And (Not n :: (l.map Not))
    :: (l.map (fun x => And [n,x]) )))
    :: ((l.map subnormalizeN).foldr (fun x y => (x.append y).dedup) []))
  | And l => ((Or (And (n :: l)
    :: (l.map (fun x => And [Not n, Not x]))))
    :: ((l.map subnormalizeN).foldr (fun x y => (x.append y).dedup) []))
  | Not i => (Or [And [n, Not i], And [Not n, i]]) :: (subnormalizeN i)
  | atom a => [Or [And [n], And [Not n]]]
termination_by n
  decreasing_by
  all_goals
    simp_wf

[Arthur Adjedj]

Here's a code with no sorries left:

import Init.Data.List
import Std.Data.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic

universe u

inductive normalizable (α : Type u) [DecidableEq α] (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : List (normalizable α pred) -> normalizable α pred
  | Or : List (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred

namespace normalizable

variable (α : Type u) [DecidableEq α] (pred : α -> Prop)

mutual

def decEqNormalizable : DecidableEq (normalizable α pred) := fun
  | atom a, atom b =>
    if h : a = b then
      .isTrue (by subst h; rfl)
    else
      .isFalse  (by intro n; injection n; apply h; assumption)
  | And a, And b | Or a, Or b =>
    let inst := decEqListNormalizable a b
    if h : a = b then
      .isTrue (by subst h; rfl)
    else
      .isFalse  (by intro n; injection n; apply h; assumption)
  | Not a, Not b =>
    let inst := decEqNormalizable a b
    if h : a = b then
      .isTrue (by subst h; rfl)
    else
      .isFalse  (by intro n; injection n; apply h; assumption)
  | Not _, Or _  |Not _, And _ | Not _, atom _
  | Or _, Not _  | Or _, And _ | Or _, atom _
  | And _, Not _ | And _, Or _ | And _, atom _
  | atom _, Not _| atom _, And _| atom _, Or _ =>
    .isFalse (by intro h; injection h)


def decEqListNormalizable : DecidableEq (List (normalizable α pred)) := fun
  | [],[] => .isTrue rfl
  | hd₁::tl₁, hd₂::tl₂ =>
      let inst₁ := decEqNormalizable hd₁ hd₂
      let inst₂ := decEqListNormalizable tl₁ tl₂
      if h₁ : hd₁ = hd₂ then
          if h₂ : tl₁ = tl₂ then .isTrue (by subst h₁ h₂; rfl)
          else .isFalse (by intro n; injection n; apply h₂; assumption)
      else
        .isFalse (by intro n; injection n; apply h₁; assumption)
  | [],_::_ | _::_,[] => .isFalse (by intro h; injection h)

end

def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And l => (l.attach.map (fun ⟨x,_⟩ => toProp x)).foldr (· ∧ ·) True
  | Or l => (l.attach.map (fun ⟨x,_⟩ => toProp x)).foldr (· ∨ ·) False
  | Not n => ¬(toProp n)

def subnormalizeN (n : normalizable α pred) [DecidableEq (normalizable α pred)] : List (normalizable α pred) :=
  match n with
  | Or l => ((Or (And (Not n :: (l.attach.map fun x => Not x.val))
    :: (l.map (fun x => And [n,x]) )))
    :: ((l.attach.map fun ⟨x,_⟩ => subnormalizeN x).foldr (fun x y => (x.append y).dedup) []))
  | And l => ((Or (And (n :: l)
    :: (l.attach.map (fun x => And [Not n, Not x]))))
    :: ((l.attach.map fun ⟨x,_⟩ => subnormalizeN x).foldr (fun x y => (x.append y).dedup) []))
  | Not i => (Or [And [n, Not i], And [Not n, i]]) :: (subnormalizeN i)
  | atom a => [Or [And [n], And [Not n]]]

[Jared green]

i put the code on github.
[](url)