filtering on a predicate with quantifiers

Stream: new members

[Jared green]

i'm still working on what i was yesterday, this is the first issue i'm stuck on.

structure bitnode :=
  mk :: (value : bool)
  (indices : list (ℕ × ℕ)) --these pointers indicate what it is connected to
  (isconstant : bool)
  (considered : bool)

structure gatenode :=
  mk :: (valence : ℕ)
  (possib : list ( vector bool valence))
  (state : bool × (vector (bool) valence)) --the fst of this indicates that the front of consideration has passed the node
  (indices : vector ℕ valence)

def tables (s:satnet)(g: ℕ ) : list ℕ × list (list bool) :=  --make a table listing all the ways that nextbits could be,
                                                              --given the last table in s.tablesequence and the gate at index g
let set: list ℕ  :=
list.erase_dup (list.append s.nextbits ((([g].filter_map (list.nth s.gts)).filter (λx,true) ).bind (λx,x.indices.1)) )
in
  (set,(
    let
    subset : list (list bool) :=
    list.filter (λx ,(        --why does this fail?
      ∀ a ∈ s.bts, b, c: ℕ , d  ∈  ([nat.sub s.tablesequence.length 1].filter_map(list.nth s.tablesequence) ).head.2,
      list.nth s.bts (list.nth (([g].filter_map(list.nth s.gts)).head.indices.1) b) = a
      → list.nth s.bts (list.nth (([nat.sub s.tablesequence.length 1].filter_map(list.nth s.tablesequence) ).head.1) c) = a
      → ¬ list.nth d c = x
      ) )
     (gatenode.possib (list.nth s.gts g)),
    expset : list list bool := list.foldr λz,(list.concat z) [] (list.map λx,( list.map λy,(list.append x y))
    (prod.snd (list.nth s.tablesequence (nat.sub (list.length s.tablesequence) 1))) (subset))
    in
    list.erase_dup (list.transpose (list.map prod.snd (list.erase_dup ( list.filter (λx,( (list.fst x ∈ (set))))
    list.zip ( list.append (prod.fst (list.nth s.tablesequence (nat.sub (list.length s.tablesequence) 1)))
    (gatenode.indices (list.nth s.gts g)) ) list.transpose (list.erase_dup expset) ) ) ) )
  ))

[Mario Carneiro]

you are missing some imports

[Jared green]

the imports are exactly the same as before. what am i missing?

[Mario Carneiro]

when making a #mwe it is good to put all the imports in, instead of making people follow along with the history, especially if you change topics/streams

[Mario Carneiro]

Here's some cleanup; the types aren't quite working yet. I don't know how you can write so much code with such a high density of syntax errors... You should address the syntax errors before you continue on to more stuff, or else you will just get uninformative errors from lean

import data.list
import data.vector.basic
import data.prod
open classical

variables a b c d: Type

@[derive inhabited]
structure bitnode :=
  mk :: (value : bool)
  (indices : list (ℕ × ℕ)) --these pointers indicate what it is connected to
  (isconstant : bool)
  (considered : bool)

@[derive inhabited]
structure gatenode :=
  mk :: (valence : ℕ)
  (possib : list ( vector bool valence))
  (state : bool × (vector (bool) valence)) --the fst of this indicates that the front of consideration has passed the node
  (indices : vector ℕ valence)

structure satnet :=  --i use an undirected graph representation of a sat instance,
                     --implemented as lists with indices as pointers
mk:: (bts : list bitnode)(gts : list gatenode)
(nextbits : list ℕ)(nextgates : list ℕ)(table : list ℕ × list (list bool))
(tablesequence: list (list ℕ × list (list bool)))

def tables (s:satnet)(g: ℕ ) : list ℕ × list (list bool) :=  --make a table listing all the ways that nextbits could be,
                                                              --given the last table in s.tablesequence and the gate at index g
let set: list ℕ :=
  list.erase_dup (s.nextbits ++ (([g].filter_map (list.nth s.gts)).filter (λx,true) ).bind (λx,x.indices.1))
in
  (set,
    let
    subset : list (list bool) :=
      (gatenode.possib (list.inth s.gts g)).filter $ λ x,
        ∀ (a ∈ s.bts) (b c: ℕ) (d ∈ (s.tablesequence.inth (s.tablesequence.length - 1)).2),
         s.bts.inth (list.inth (([g].map (list.inth s.gts)).head.indices.1) b) = a
        →  s.bts.inth (list.inth (s.tablesequence.inth (s.tablesequence.length - 1)).1 c) = a
        → ¬ list.inth d c = x,
    expset : list (list bool) :=
      list.foldr (λz, list.concat z) [] $
        list.map (λx, list.map (λy, x ++ y))
          (s.tablesequence.inth (list.length s.tablesequence - 1)).2 subset
    in
    list.erase_dup (list.transpose (list.map prod.snd (list.erase_dup ( list.filter (λx,( (list.fst x ∈ (set))))
    list.zip ( list.append (prod.fst (list.nth s.tablesequence (nat.sub (list.length s.tablesequence) 1)))
    (gatenode.indices (list.nth s.gts g)) ) list.transpose (list.erase_dup expset) ) ) ) )
  ))

[Mario Carneiro]

By using @[derive inhabited] on all the types, it means we can use list.inth instead of struggling with list.nth all the time

[Mario Carneiro]

Okay, here's a version that works, except for a decidability requirement because you are filtering by a predicate that has an unbounded quantification ∀ (b c: ℕ), in it

-- make a table listing all the ways that nextbits could be,
-- given the last table in s.tablesequence and the gate at index g
def tables (s : satnet) (g : ℕ) : list ℕ × list (list bool) :=
let set: list ℕ := (s.nextbits ++ (s.gts.inth g).indices.1).erase_dup in
(set,
  let subset : list (list bool) :=
    ((s.gts.inth g).possib.map subtype.val).filter $ λ x,
      ∀ (a ∈ s.bts) (b c: ℕ) (d ∈ s.tablesequence.last'.iget.2),
      s.bts.inth ((s.gts.inth g).indices.1.inth b) = a
      →  s.bts.inth (s.tablesequence.last'.iget.1.inth c) = a
      → ¬ list.inth (sorry /-d-/) c = x in
  let expset : list (list bool) :=
    subset.bind $ λ x, s.tablesequence.last'.iget.2.map (λ y, x ++ y) in
  list.erase_dup $ list.transpose $ list.map prod.snd $ list.erase_dup $
  list.filter (λ x, x.1 ∈ set) $
    (s.tablesequence.last'.iget.1 ++ (s.gts.inth g).indices.1).zip expset.erase_dup.transpose)

[Mario Carneiro]

also the use of d at the sorry is a type error

[Jared green]

why isnt d being used directly there

[Mario Carneiro]

I commented it out since it's not the right type

[Mario Carneiro]

I don't understand the code well enough to suggest a fix

[Mario Carneiro]

but d has type list bool and the sorry has type list (list bool)

[Mario Carneiro]

it could also be that x has the wrong type (it is list bool)

[Jared green]

both x and d should have type list bool

[Mario Carneiro]

then what does it mean to say d.inth c = x?

[Jared green]

with d being the row of the truth table, c picks out the column

[Mario Carneiro]

that's a bool

[Jared green]

whats a bool

[Mario Carneiro]

so why is it being equated to x which is a list bool

[Mario Carneiro]

d.inth c = x is a type error

[Jared green]

i should have equated it to an element of x

[Jared green]

that with the index b

[Mario Carneiro]

ok, this typechecks

def tables (s : satnet) (g : ℕ) : list ℕ × list (list bool) :=
let set: list ℕ := (s.nextbits ++ (s.gts.inth g).indices.1).erase_dup in
(set,
  let subset : list (list bool) :=
    ((s.gts.inth g).possib.map subtype.val).filter $ λ x,
      ∀ (a ∈ s.bts) (b < x.length) (d ∈ s.tablesequence.last'.iget.2) (c < list.length d),
        s.bts.inth ((s.gts.inth g).indices.1.inth b) = a →
        s.bts.inth (s.tablesequence.last'.iget.1.inth c) = a →
        ¬ d.inth c = x.inth b in
  let expset : list (list bool) :=
    subset.bind $ λ x, s.tablesequence.last'.iget.2.map (λ y, x ++ y) in
  list.erase_dup $ list.transpose $ list.map prod.snd $ list.erase_dup $
  list.filter (λ x, x.1 ∈ set) $
    (s.tablesequence.last'.iget.1 ++ (s.gts.inth g).indices.1).zip expset.erase_dup.transpose)

Double check the bounds on b and c. There are two equalities of bitnodes here (a is a bitnode), so you have to derive decidable_eq on bitnode to make it work:

@[derive [inhabited, decidable_eq]]
structure bitnode :=
  mk :: (value : bool)
  (indices : list (ℕ × ℕ)) --these pointers indicate what it is connected to
  (isconstant : bool)
  (considered : bool)