Things for which there was no documentation i could find

Stream: Is there code for X?

[Jared green]

I was trying to write a program in the latest version of lean 3, and here are certain things I couldn’t find documentation for, causing a bunch of errors.
-creating and casting vectors as lists
-casting option a’s as a‘s
-inhabiting a predicate as the input to a function, such as list.nth_le, that calls for it
-taking apart ordered pairs
-using list.foldr
-syntax for lambdas giving something of type a -> b rather than \Pi (x:a) : b
-syntax for let expressions
-syntax for quantifiers
-a function to do the same thing to a list of lists each the same length as is done to a matrix when it is transposed
-a higher order function to apply a given function an arbitrary number of times
-syntax for declaring refinement types and creating elements thereof
-expressing and proving worst case asymptotic runtimes for a program written in the purely functional language, according to the tm2 model(this is part of my ultimate goal)

[Mario Carneiro]

-creating and casting vectors as lists

Create a vector with docs#vector.nil and docs#vector.cons, convert it to a list with vec.1

-casting option a’s as a‘s

Can't do it, that's unsound. But docs#option.get will get the value if it is not none, and docs#option.iget will get the value or a default value of the type

-inhabiting a predicate as the input to a function, such as list.nth_le, that calls for it

The easiest way is dec_trivial, although it doesn't always apply. In general, well it's a proof goal

-taking apart ordered pairs

You can use let (a, b) := pair in ... or pair.1 and pair.2 (which are short for docs#prod.fst and docs#prod.snd)

-using list.foldr

It folds a function from right to left, i.e. foldr f z [1, 2, 3] = f 1 (f 2 (f 3 z))

-syntax for lambdas giving something of type a -> b rather than \Pi (x:a) : b

a -> b is the same as \Pi (x:a) : b, and there is only one lambda

-syntax for let expressions

let x : type := value in expr

-syntax for quantifiers

\forall x : type, prop, \exists x : type, prop

-a function to do the same thing to a list of lists each the same length as is done to a matrix when it is transposed

docs#list.transpose

-a higher order function to apply a given function an arbitrary number of times

docs#nat.iterate

-syntax for declaring refinement types and creating elements thereof

docs#subtype, docs#subtype.mk. The syntax is {x // p x} for the type, ⟨x, h⟩ for creating an element of the type, and p.1 and p.2 for extracting the components

-expressing and proving worst case asymptotic runtimes for a program written in the purely functional language, according to the tm2 model(this is part of my ultimate goal)

It's not possible to prove runtime bounds on programs written in pure lean, because runtime is not preserved by lean equality. But for functions which are deeply embedded i.e. in the TM2 model it is possible. Unfortunately the infrastructure isn't there yet

[Jared green]

dec_trivial isn’t working.
vec.l isn’t working.
Prod.and and prod.fast works in some places, but where it doesn’t, neither does pair.1 and pair.2 .
I have a universal quantifier that looks like as follows, where apparently d is an unknown identifier:
\forall a, b, c, d : \nat, <pred>
Is it in fact valid to use the \in symbol to check for the presence of a given value in a list?
Is there a function to find where it is afterward?
When using foldr, and the function I’m using is && or +(nat), how do i do that?
And, in some places lean seems to expect a (Type: Type 1) rather than an element of the type i thought it should. Why?

[Jared green]

*thats prod.snd and prod.fst

[Yaël Dillies]

It's hard to help you without seeing your code. Would you mind providing a #mwe?

[Kevin Buzzard]

I think that instead of asking 100 questions it might be easier to ask fewer questions and back them all up with a #mwe . Nobody can debug "dec_trivial isn't working" with no further information -- it works for me

[Jared green]

this is the nearly first 250 of nearly 500 lines i have written. not sure if it counts as an mwe, for it doesnt in fact work. the rest in the next comment:

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

variables a b c: Type

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))--i dont know how to create vectors or cast them as lists
(state : bool × (vector (bool) valence)) --the fst of this indicates that the front of consideration has passed the node
(indices : vector ℕ valence)

def reversible (a : gatenode) : Prop :=
(∀ b c d : ℕ, (b < a.possib.length → c < a.possib.length → d < a.valence
→ (
--the entry is fully determined by all but one bit. represented in haskell like so:
--(
--remove_nth
--((a.possib))!!b d
--==
--remove_nth
--( (a.possib))!!c d
--)
--<->
(
(((a.possib))!!b)!!d
==
((a.possib))!!c)!!d
)
)

)

)
)
--the types of gates: not, and 3-unique, which is complete
----an AND gate can be constructed as follows:
-- bits 1-8. inputs to bit 3,7. output bit 5. 3unique(1,2,3), 3unique(4,5,6), NOT(7,8), 3unique(1,4,7), 3unique(2,5,8), NOT(3,6)
-- the OR gate can be constructed the same way, with the output put through a NOT, and the inputs at 6,8.
--therefore 3-unique is functionally complete.
def mknot (c: vector ℕ 2) : gatenode :=
{valence := 2, possib := [vector.cons ff (vector.cons tt vector.nil),vector.cons tt (vector.cons ff vector.nil)],
state := (ff,vector.cons ff (vector.cons tt vector.nil)), indices := c}

def mk3unique (c: vector ℕ 3) : gatenode :=
{valence := 3, possib := [vector.cons ff(vector.cons ff (vector.cons tt vector.nil)),
vector.cons ff(vector.cons tt(vector.cons ff vector.nil)),
vector.cons tt(vector.cons ff(vector.cons ff vector.nil))],
state := (ff,(vector.cons ff(vector.cons ff(vector.cons tt vector.nil)))), indices := c}

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)))

--all indices must be within range.
--the corresponding function is implemented in haskell like so:

--vetnet :: satnet -> bool
--vetnet a =
--fold && map (\x->(fold && map (\y->(bts a !!(indices((gts a) !! (fst y))!! (snd y))== y))(indices x))) (bts a)
--&&
--fold && map (\x->(fold && map (\y->(fold || map (\z->(((gts a)!! (fst z)) == x && (indices((gts b)!! (fst z))!!
--(snd z))== y)) (indices y)!! y )) indices x))(gts a)

def solv1 (s : satnet) :satnet := --start by, if possible, considering the bits that are constant
let cond:Prop := (--should be a true prop if there are no nodes satisfying the lambda expression
list.length
(
list.filter
(λx,(
((bitnode.isconstant x) = tt)
))
s.bts
) = 0
) ,
set:list ℕ := list.map prod.fst
(list.filter
(
(λx,(
((bitnode.isconstant x) = tt)
)) ∘ prod.snd
)
(
list.zip
(
list.range
(
list.length s.bts
)
)
s.bts
)) in
{bts := s.bts,
gts := s.gts,
nextbits :=
if cond
then [0]
else set,
nextgates := s.nextgates,
table := s.table,
tablesequence:= []
}

def solv2 (s: satnet) : satnet := --get the first gate and table on the list
let set:list ℕ := list.erase_dup --actually leaves in the last copy of the set of duplicates, but is nonetheless consistent
( list.map
(
list.foldr
(
list.append
(
list.map prod.fst ∘ bitnode.indices
(
list.filter (λx,( ¬ (bitnode.considered x) = tt))
(
list.map
(λx,(
list.nth_le s.bts x (dec_trivial)
))
s.nextbits
)
)
)
)
)
)
in
{ bts := s.bts,
gts := s.gts,
nextbits := s.nextbits,
nextgates:=
if list.length s.nextgates = 0 then if list.length set = 0 then [0] else [list.head set] else s.nextgates,
table := if list.length s.nextgates = 0 then if list.length set = 0 then
(vec.l gatenode.indices (list.nth_le s.gts (list.head set) dec_trivial ),
list.map vec.l (gatenode.possib (list.nth_le s.gts (list.head set) dec_trivial) ))
else (vec.l gatenode.indices (list.nth_le s.gts (list.head set) dec_trivial),
list.map vec.l (gatenode.possib (list.nth_le s.gts (list.head set) dec_trivial))) else s.table,

tablesequence := if list.length s.nextgates = 0
then if list.length set = 0
then [(vec.l (gatenode.indices (list.head s.gts)), list.map vec.l (gatenode.possib (list.head s.gts)))]
else [(vec.l (gatenode.indices (list.nth_le s.gts (list.head set) dec_trivial)),
list.map vec.l (gatenode.possib (list.nth_le s.gts (list.head set) dec_trivial)))]
else s.tablesequence
}

def solv3 (s:satnet) : satnet := --remove those bits that the front of consideration has passed from nextbits
{
bts := s.bts, gts := s.gts, nextbits :=
list.filter
(λy,(
((
list.foldr
(λz,λw,(z && w))
(list.map
(λx:ℕ,(
pair.1 --im not sure what im doing wrong when it comes to taking ordered pairs apart,
-- as that seems to be the source of most of the errors in the file0
gatenode.state
(list.nth
s.gts
x
))
(
list.map
prod.fst
(
bitnode.indices
y
)
) = tt
)
)
))
))
(list.erase_dup
(
list.foldr
(
list.append
(
list.map (λx:gatenode,(vec.l gatenode.indices x))
(
list.filter
(λx,( ¬ (
prod.fst (gatenode.state x)
) = tt))
(
list.map --how to turn an option a to an a?
(λx,(
list.nth_le s.gts x dec_trivial
))
s.nextbits
)
)
)
)
))
, nextgates := s.nextgates,
table := s.table,
tablesequence := s.tablesequence
}

def size (l: list (list a)) : ℕ :=
(list.foldr (λx,λy,(nat.add x y)) (list.map list.length l))

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 (vec.l gatenode.indices (list.nth_le s.gts g dec_trivial))
in
(set,(
--implement like so:
--intersect set with that of nth tablesequence length - 1
let
--the states that are compatible
subset : list list bool :=
list.filter (λx,( --why is d unknown?
∀ a, b, c, d : ℕ, a < (list.length s.bts) → b < gatenode.valence (list.nth_le s.gts g dec_trivial) → c < list.length prod.fst
(list.nth s.tablesequence (nat.sub (list.length s.tablesequence) 1))
→ list.nth_le (gatenode.indices list.nth s.gts) b dec_trivial = list.nth_le (prod.fst
(list.nth_le s.tablesequence (nat.sub (list.length s.tablesequence) 1) dec_trivial)) c dec_trivial
→ d < list.length (prod.snd
(list.nth_le s.tablesequence (nat.sub (list.length s.tablesequence) 1) dec_trivial))
→ ¬ list.nth_le (list.nth_le (prod.snd
(list.nth s.tablesequence (nat.sub (list.length s.tablesequence) 1))) c dec_trivial) d dec_trivial = vector.nth_le x b dec_trivial
)

[Jared green]

and here is the rest:

) (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 --by transpose, i mean like matrix transposition
(
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
)
)
)
)
)
))

def solv4 (s:satnet) : satnet := --construct the smallest table for any choice in how the front of consideration is to advance
{bts := s.bts,
gts := s.gts,
nextbits := s.nextbits,
nextgates := list.concat
s.nextgates
(
list.argmin
(
size (prod.snd
(λx,(tables s x)))
)
(
list.filter
(λx,(¬ ((prod.fst (gatenode.state (list.nth_le s.gts x dec_trivial))= tt) ∨ x ∈ s.nextgates)))
(list.range (list.length s.gts))
)
),
table := list.argmin λx,(size (prod.snd x)) (list.map (λx,(tables s x)) (list.range (list.length s.gts))),
--the one thing i'm not sure on,
--the maximum number of entries in this table, if im correct,
-- grows no faster than the number of gates
--sketch:
--initially, the front of consideration is fully determined until it reaches the edge of a bubble
-- a bubble is here defined as a subset of the satnet s where determination on the outside has no bearing on the inside, though not necessarily vice versa
--the edge of a bubble is formed by one ore more cycles of gates connected to bits on the inside, and each one has a single line outwards
--for each cycle, there are at most two distinct states the whole cycle can be in
-- the most efficient traversal through that is to consider the consequences of one cycle at a time,
--as that keeps the number of entries below some constant
--it will take an automated proof search to prove that this is always possible

--though i do know that it is definitely subexponential,
-- at most 2^(sqrt(n))
--sketch:
--the width of the front of consideration grows linearly and then shrinks linearly
-- from one gate to its maximum than back down to just one again
--for the maximum to be the absolute worst case, the system must approximate a square with the disjoint subsets that the front passes through in layers
--the maximum width then is sqrt(2n)
--the maximum number of states that can take on is O(2^(sqrt(2n)))
--qed, therefore the exponential time hypothesis is false
tablesequence := s.tablesequence
}

def solv5 (s:satnet) : satnet := --place the new table in the squence
{bts := s.bts,
gts := s.gts,
nextbits := s.nextbits,
nextgates := s.nextgates,
table := s.table,
tablesequence := list.concat s.tablesequence s.table
}

--say that the bitnodes and gatenodes that the front of consideration has passed are considered
def reconsider (s:satnet)(b:ℕ ) : bitnode :=
{
value := bitnode.value (list.nth_le s.bts b dec_trivial),
indices := bitnode.indices (list.nth_le s.bts b dec_trivial),
isconstant := bitnode.isconstant (list.nth_le s.bts b dec_trivial),
considered :=
if
list.foldr
(λz,λw,(z && w))
(list.map
(λx,(
prod.fst x ∈ s.nextgates
))
(
bitnode.indices
(list.nth_le s.bts b dec_trivial)
) )
then
tt
else
bitnode.considered
(list.nth_le s.bts b dec_trivial)
}

def solv6 (s:satnet) : satnet :=
{bts := list.map (λx,(reconsider s x)) (list.range (list.length s.bts)),
gts := s.gts,
nextbits := s.nextbits,
nextgates := s.nextgates,
table := s.table,
tablesequence := s.tablesequence
}

def greconsider (s:satnet)(g:ℕ )(c:bool) : gatenode :=
{valence := gatenode.valence (list.nth_le s.gts g dec_trivial),
possib := gatenode.possib (list.nth_le s.gts g dec_trivial),
indices := gatenode.indices (list.nth_le s.gts g dec_trivial),
state :=
(
(
if
c
then
tt
else
(
prod.fst
(gatenode.state (list.nth_le s.gts g dec_trivial))
)
),
(
prod.snd
(gatenode.state (list.nth_le s.gts g dec_trivial))
)
)
}

def solv7 (s:satnet) : satnet :=
let set:list ℕ := list.filter
(λy,(
((
list.foldr
(λz,λw,(z && w))
(list.map
(λx,(
bitnode.considered x
) = tt)
(vec.l (gatenode.indices (list.nth_le s.gts y dec_trivial)))
)
) )
))
(
list.range
(list.length s.gts)
)
in
{bts := s.bts,
gts := list.map (λx,(greconsider s x (x ∈ set))) (list.range (list.length s.gts))
,nextbits := s.nextbits,
nextgates := list.filter (λx,(¬ (x ∈ set))) s.nextgates,
table := s.table,
tablesequence := s.tablesequence
}

def solvcycle : satnet -> satnet := --the cycle starts in solv3.
solv7 ∘ solv6 ∘ solv5 ∘ solv4 ∘ solv3

def solvcert (s:satnet ): satnet := --this is the information required to 'certify' satisfiability without a witness
(nat.iterate solvcycle (nat.sub (list.length s.gts) 1)) ((solv2 ∘ solv1) s)

def solvdecide (s:satnet): bool := list.length (prod.snd (satnet.table (solvcert s))) > 0 --this 'solves the decision problem'

def solvretract1 (s:satnet) : satnet := --pick an entry, possibly random, in the last table and commit to it
-- choose a nat in 0..length (snd (last table), maybe randomly
let choicen : ℕ :=
random (0, list.length prod.snd s.table)
in
{bts :=
--set the value of each bitnode to that in the entry corresponding to the number previously chosen
list.map
(λx:ℕ,
{value := if x ∈ prod.fst s.table
then list.nth_le (list.nth_le (prod.snd s.table) choicen dec_trivial) (list.indexof x (prod.fst s.table)) dec_trivial --surely there is a function that does this
else bitnode.value (list.nth_le s.bts x dec_trivial),
indices := bitnode.indices (list.nth_le s.bts x dec_trivial),
isconstant:= bitnode.isconstant (list.nth_le s.bts x dec_trivial),
considered := bitnode.considered (list.nth_le s.bts x dec_trivial)})
(list.range (list.length s.bts)),

gts := --same here
--placeholder
s.gts
-- if all the bits connected to a gate are in the last table then set the state to the values in the table entry

,
nextbits := s.nextbits, nextgates := s.nextgates,
table := (prod.fst s.table, list.nth_le (pair.2 s.table) choicen dec_trivial),
tablesequence := s.tablesequence
}

def solvretract2 (s:satnet ) : satnet := -- remove the entries incompatible with the table from which we are puuling back
{bts := s.bts,
gts := s.gts,
nextbits := s.nextbits,
nextgates := s.nextgates,
table := s.table,
tablesequence :=
(
list.concat
(list.remove_nth (s.tablesequence)
( nat.sub (list.length (s.tablesequence)) 1)),
list.filter
(
λx,(
(
∀ b, c, d : ℕ ,
b < list.length (prod.fst s.table)
→ c < list.length x
→ list.nth x c = d
→ list.nth_le (prod.fst s.table) b dec_trivial = d
→ list.nth_le (prod.snd s.table) b dec_trivial = list.nth_le x c dec_trivial
)
)
)
(list.nth_le s.tablesequence (nat.sub (list.length s.tablesequence) 1) dec_trivial)
)
}

def solvretract3 (s:satnet) : satnet := --pop the last table in the sequence off
{bts := s.bts,
gts := s.gts,
nextbits := s.nextbits,
nextgates := s.nextgates,
table := list.nth_le s.tablesequence ( nat.sub (list.length s.tablesequence) 1) dec_trivial,
tablesequence := list.remove_nth s.tablesequence (nat.sub (list.length s.tablesequence) 1)}

def solvwitness (s:satnet): satnet := --this solves the 'function problem'
(nat.iterate (λx,(solvretract3 (solvretract2 ( solvretract1 x))))(list.length s.gts) ) ((solvcert) s)

[Reid Barton]

Use #backticks so that the formatting will be preserved (you can edit your messages).

[Jared green]

trying it again:

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

variables a b c d: Type



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 reversible (a : gatenode) : Prop :=
  (∀ b c d : ℕ, (b < a.possib.length → c < a.possib.length → d < a.valence
    → (
          --the entry is fully determined by all but one bit. represented in haskell like so:
      --(
                --remove_nth
                --((a.possib))!!b  d
                --==
                --remove_nth
                --( (a.possib))!!c  d
            --)
            --<->
            (
                (((a.possib))!!b)!!d
                ==
                ((a.possib))!!c)!!d
            )
      )

    )
   )
  )
--the types of gates: not, and 3-unique, which is complete
----an AND gate can be constructed as follows:
            -- bits 1-8. inputs to bit 3,7. output bit 5. 3unique(1,2,3), 3unique(4,5,6), NOT(7,8), 3unique(1,4,7), 3unique(2,5,8), NOT(3,6)
            -- the OR gate can be constructed the same way, with the output put through a NOT, and the inputs at 6,8.
            --therefore 3-unique is functionally complete.
def mknot (c: vector ℕ 2) : gatenode :=
  {valence := 2, possib := [vector.cons ff (vector.cons tt vector.nil),vector.cons tt (vector.cons ff vector.nil)],
  state := (ff,vector.cons ff (vector.cons tt vector.nil)), indices := c}

def mk3unique (c: vector ℕ 3) : gatenode :=
{valence := 3, possib := [vector.cons ff(vector.cons ff (vector.cons tt vector.nil)),
vector.cons ff(vector.cons tt(vector.cons ff vector.nil)),
vector.cons tt(vector.cons ff(vector.cons ff vector.nil))],
  state := (ff,(vector.cons ff(vector.cons ff(vector.cons tt vector.nil)))), indices := c}

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)))

--all indices must be within range.
--the corresponding function is implemented in haskell like so:

--vetnet :: satnet -> bool
--vetnet a =
    --fold && map (\x->(fold && map (\y->(bts a !!(indices((gts a) !! (fst y))!! (snd y))== y))(indices x))) (bts a)
    --&&
    --fold && map (\x->(fold && map (\y->(fold || map (\z->(((gts a)!! (fst z)) == x && (indices((gts b)!! (fst z))!!
  --(snd z))== y)) (indices y)!! y )) indices x))(gts a)


def solv1 (s : satnet) :satnet := --start by, if possible, considering the bits that are constant
let cond:Prop := (
    list.length
    (
      list.filter
      (λx,(
         ((bitnode.isconstant x) = tt)
      ))
      s.bts
    ) = 0
  ) ,
  set:list ℕ  := list.map prod.fst
  (list.filter
  (
    (λx,(
       ((bitnode.isconstant x) = tt)
    )) ∘ prod.snd
  )
  (
    list.zip
    (
      list.range
      (
        list.length s.bts
      )
    )
    s.bts
  )) in
{bts := s.bts,
gts := s.gts,
  nextbits :=
  if cond
  then [0]
  else set,
  nextgates := s.nextgates,
  table := s.table,
  tablesequence:= []
  }

def solv2 (s: satnet) : satnet := --get the first gate and table on the list
let set:list ℕ := list.erase_dup  --actually leaves in the last copy of the set of duplicates, but is nonetheless consistent
  ( list.map
    (
      list.foldr
      (
        list.append
        (
          list.map prod.fst ∘ bitnode.indices
          (
            list.filter (λx,( ¬ (bitnode.considered x) = tt))
            (
              list.map
              (λx,(
                list.nth_le s.bts x (dec_trivial)
              ))
              s.nextbits
            )
          )
        )
      )
    )
  )
  in
{ bts := s.bts,
gts := s.gts,
nextbits := s.nextbits,
nextgates:=
  if list.length s.nextgates = 0 then if list.length set = 0 then [0] else [list.head set] else s.nextgates,
  table := if list.length s.nextgates = 0 then if list.length set = 0 then
   (vec.l gatenode.indices (list.nth_le  s.gts (list.head set) dec_trivial ),
  list.map vec.l (gatenode.possib (list.nth_le s.gts (list.head set) dec_trivial) ))
  else (vec.l gatenode.indices (list.nth_le s.gts (list.head set) dec_trivial),
  list.map vec.l (gatenode.possib (list.nth_le s.gts (list.head set) dec_trivial))) else s.table,

  tablesequence := if list.length s.nextgates = 0
  then if list.length set = 0
  then [(vec.l (gatenode.indices (list.head s.gts)), list.map vec.l (gatenode.possib (list.head s.gts)))]
  else [(vec.l (gatenode.indices (list.nth_le s.gts (list.head set) dec_trivial)),
  list.map vec.l (gatenode.possib (list.nth_le s.gts (list.head set) dec_trivial)))]
  else s.tablesequence
}

def solv3 (s:satnet) : satnet :=  --remove those bits that the front of consideration has passed from nextbits
{
  bts := s.bts, gts := s.gts, nextbits :=
  list.filter
  (λy,(
     ((
      list.foldr
      (λz,λw,(z && w))
      (list.map
        (λx:ℕ,(
          pair.1
          gatenode.state
          (list.nth
          s.gts
          x
        ))
          (
            list.map
            prod.fst
            (
              bitnode.indices
              y
            )
          ) = tt
        )
      )
    ))
  ))
  (list.erase_dup
  (
    list.foldr
    (
      list.append
      (
        list.map (λx:gatenode,(vec.l gatenode.indices x))
        (
          list.filter
          (λx,( ¬ (
            prod.fst (gatenode.state x)
          ) = tt))
          (
            list.map
            (λx,(
              list.nth_le s.gts x dec_trivial
            ))
            s.nextbits
          )
        )
      )
    )
  ))
  , nextgates := s.nextgates,
  table := s.table,
  tablesequence := s.tablesequence
}

def size (l: list (list a)) : ℕ :=
 (list.foldr (λx,λy,(nat.add x y)) (list.map list.length l))

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 (vec.l gatenode.indices (list.nth_le s.gts g dec_trivial))
in
  (set,(
    --implement like so:
    --intersect set with that of nth tablesequence length - 1
    let
    --the states that are compatible
    subset : list list bool :=
    list.filter (λx,(        --why is d unknown?
      ∀ a, b, c, d : ℕ, a < (list.length s.bts) → b < gatenode.valence (list.nth_le s.gts g dec_trivial) → c < list.length prod.fst
        (list.nth s.tablesequence (nat.sub (list.length s.tablesequence) 1))
         → list.nth_le (gatenode.indices list.nth s.gts) b dec_trivial =  list.nth_le (prod.fst
         (list.nth_le s.tablesequence (nat.sub (list.length s.tablesequence) 1) dec_trivial)) c dec_trivial
         → d < list.length (prod.snd
         (list.nth_le s.tablesequence (nat.sub (list.length s.tablesequence) 1) dec_trivial))
         → ¬ list.nth_le (list.nth_le (prod.snd
         (list.nth s.tablesequence (nat.sub (list.length s.tablesequence) 1))) c dec_trivial) d dec_trivial = vector.nth_le x b dec_trivial
        )

    ) (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
            )
          )
        )
      )
    )
  ))

[Jared green]

respond to this comment please.

def solv4 (s:satnet) : satnet := --construct the smallest table for any choice in how the front of consideration is to advance
{bts := s.bts,
 gts := s.gts,
 nextbits := s.nextbits,
  nextgates := list.concat
  s.nextgates
  (
    list.argmin
    (
     size (prod.snd
      (λx,(tables s x)))
    )
    (
      list.filter
      (λx,(¬ ((prod.fst (gatenode.state (list.nth_le s.gts x dec_trivial))= tt) ∨  x ∈ s.nextgates)))
      (list.range (list.length s.gts))
    )
  ),
   table := list.argmin λx,(size (prod.snd x)) (list.map (λx,(tables s x)) (list.range (list.length s.gts))),
  --the one thing i'm not sure on,
  --the maximum number of entries in this table, if im correct,
  -- grows no faster than the number of gates
  --sketch:
  --initially, the front of consideration is fully determined until it reaches the edge of a bubble
  -- a bubble is here defined as a subset of the satnet s where determination on the outside has no bearing on the inside, though not necessarily vice versa
  --the edge of a bubble is formed by one ore more cycles of gates connected to bits on the inside, and each one has a single line outwards
  --for each cycle, there are at most two distinct states the whole cycle can be in
  -- the most efficient traversal through that is to consider the consequences of one cycle at a time,
  --as that keeps the number of entries below some constant
  --it will take an automated proof search to prove that this is always possible

  --though i do know that it is definitely subexponential,
  -- at most 2^(sqrt(n))
  --sketch:
  --the width of the front of consideration grows linearly and then shrinks linearly
  -- from one gate to its maximum than back down to just one again
  --for the maximum to be the absolute worst case, the system must approximate a square with the disjoint subsets that the front passes through in layers
  --the maximum width then is sqrt(2n)
  --the maximum number of states that can take on is O(2^(sqrt(2n)))
  --qed, therefore the exponential time hypothesis is false
  tablesequence := s.tablesequence
}

def solv5 (s:satnet) : satnet :=   --place the new table in the squence
{bts := s.bts,
gts := s.gts,
nextbits := s.nextbits,
nextgates := s.nextgates,
table := s.table,
tablesequence := list.concat s.tablesequence s.table
}

--say that the bitnodes and gatenodes that the front of consideration has passed are considered
def reconsider (s:satnet)(b:ℕ ) : bitnode :=
  {
    value := bitnode.value (list.nth_le s.bts b dec_trivial),
    indices := bitnode.indices (list.nth_le s.bts b dec_trivial),
    isconstant := bitnode.isconstant (list.nth_le s.bts b dec_trivial),
    considered :=
    if
    list.foldr
    (λz,λw,(z && w))
    (list.map
    (λx,(
     prod.fst x ∈ s.nextgates
    ))
    (
      bitnode.indices
      (list.nth_le s.bts b dec_trivial)
    ) )
    then
    tt
    else
    bitnode.considered
    (list.nth_le s.bts b dec_trivial)
  }

def solv6 (s:satnet) : satnet :=
{bts := list.map (λx,(reconsider s x)) (list.range (list.length s.bts)),
gts := s.gts,
nextbits := s.nextbits,
nextgates := s.nextgates,
table := s.table,
tablesequence := s.tablesequence
}

def greconsider (s:satnet)(g:ℕ )(c:bool) : gatenode :=
{valence := gatenode.valence (list.nth_le s.gts g dec_trivial),
possib := gatenode.possib (list.nth_le s.gts g dec_trivial),
indices := gatenode.indices (list.nth_le s.gts g dec_trivial),
state :=
(
  (
    if
    c
    then
    tt
    else
    (
      prod.fst
      (gatenode.state (list.nth_le s.gts g dec_trivial))
    )
  ),
  (
    prod.snd
    (gatenode.state (list.nth_le s.gts g dec_trivial))
  )
)
}

def solv7 (s:satnet) : satnet :=
let set:list ℕ  := list.filter
(λy,(
  ((
    list.foldr
    (λz,λw,(z && w))
    (list.map
      (λx,(
        bitnode.considered x
      ) = tt)
      (vec.l (gatenode.indices (list.nth_le s.gts y dec_trivial)))
    )
  ) )
))
(
  list.range
  (list.length s.gts)
)
in
{bts := s.bts,
gts := list.map (λx,(greconsider s x (x ∈ set))) (list.range (list.length s.gts))
,nextbits := s.nextbits,
nextgates := list.filter (λx,(¬ (x ∈ set))) s.nextgates,
table := s.table,
tablesequence := s.tablesequence
}

def solvcycle : satnet -> satnet := --the cycle starts in solv3.
 solv7 ∘ solv6 ∘ solv5 ∘ solv4 ∘ solv3


def solvcert (s:satnet ): satnet := --this is the information required to 'certify' satisfiability without a witness
(nat.iterate  solvcycle (nat.sub (list.length s.gts) 1)) ((solv2 ∘ solv1) s)

def solvdecide (s:satnet): bool := list.length (prod.snd (satnet.table (solvcert s))) > 0  --this 'solves the decision problem'

def solvretract1 (s:satnet) : satnet :=    --pick an entry, possibly random, in the last table and commit to it
-- choose a nat in 0..length (snd (last table), maybe randomly
let choicen : ℕ :=
random  (0, list.length prod.snd s.table)
in
{bts :=
--set the value of each bitnode to that in the entry corresponding to the number previously chosen
list.map
(λx:ℕ,
{value := if x ∈ prod.fst s.table
then list.nth_le (list.nth_le (prod.snd s.table) choicen dec_trivial) (list.indexof x (prod.fst s.table)) dec_trivial --surely there is a function that does this
else bitnode.value (list.nth_le s.bts x dec_trivial),
indices := bitnode.indices (list.nth_le s.bts x dec_trivial),
isconstant:= bitnode.isconstant (list.nth_le s.bts x dec_trivial),
considered := bitnode.considered (list.nth_le s.bts x dec_trivial)})
(list.range (list.length s.bts)),

 gts := --same here
 --placeholder
 s.gts
-- if all the bits connected to a gate are in the last table then set the state to the values in the table entry

,
nextbits := s.nextbits, nextgates := s.nextgates,
table := (prod.fst s.table, list.nth_le (pair.2 s.table) choicen dec_trivial),
tablesequence := s.tablesequence
}

def solvretract2 (s:satnet ) : satnet :=  -- remove the entries incompatible with the table from which we are puuling back
{bts := s.bts,
gts := s.gts,
nextbits := s.nextbits,
nextgates := s.nextgates,
table := s.table,
tablesequence :=
  (
    list.concat
    (list.remove_nth (s.tablesequence)
    ( nat.sub (list.length (s.tablesequence)) 1)),
    list.filter
    (
      λx,(
         (
          ∀ b, c, d : ℕ ,
          b < list.length (prod.fst s.table)
          → c < list.length x
          →  list.nth x c = d
          → list.nth_le (prod.fst s.table) b dec_trivial = d
          → list.nth_le (prod.snd s.table) b dec_trivial = list.nth_le x c dec_trivial
        )
      )
    )
    (list.nth_le s.tablesequence (nat.sub (list.length s.tablesequence) 1) dec_trivial)
  )
}

def solvretract3 (s:satnet) : satnet := --pop the last table in the sequence off
{bts := s.bts,
gts := s.gts,
nextbits := s.nextbits,
nextgates := s.nextgates,
table := list.nth_le s.tablesequence ( nat.sub (list.length s.tablesequence) 1) dec_trivial,
tablesequence := list.remove_nth s.tablesequence (nat.sub (list.length s.tablesequence) 1)}

def solvwitness (s:satnet): satnet := --this solves the 'function problem'
(nat.iterate (λx,(solvretract3 (solvretract2 ( solvretract1 x))))(list.length s.gts) ) ((solvcert) s)

[Mario Carneiro]

This is not a #mwe. The interpretation of "working" here is "it demonstrates the issue you are having trouble with", i.e. it fails in the expected way. But "minimal" is also important. Remove all definitions that are not relevant to the error, by stubbing things out (put sorry anywhere you can). And if you comment your code, make sure the comments are relevant to the error, especially if there are multiple lean errors in the document

[Mario Carneiro]

I said vec.1 not vec.l by the way

[Mario Carneiro]

and vec is supposed to be the variable of type vector that you have

[Mario Carneiro]

the underlying function is subtype.val

[Mario Carneiro]

I should also note that in lean we generally avoid point-free programming; things like dot-notation don't work in point-free style and the composition operator can interfere with proofs

[Mario Carneiro]

Here's a leanified version of your file through solv1:

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

variables (a b c d : Type)

structure bitnode :=
(value : bool)
(indices : list (ℕ × ℕ))
(isconstant : bool)
(considered : bool)

structure gatenode :=
(valence : ℕ)
(possib : list (vector bool valence))
(state : bool × vector bool valence)
(indices : vector ℕ valence)

def reversible (a : gatenode) : Prop :=
∀ v w ∈ a.possib, ∀ i < a.valence,
  (v:vector _ _).1.remove_nth i = (w:vector _ _).1.remove_nth i → v = w

def mknot (c: vector ℕ 2) : gatenode :=
{ valence := 2,
  possib := [ff ::ᵥ ff ::ᵥ vector.nil, tt ::ᵥ ff ::ᵥ vector.nil],
  state := (ff, ff ::ᵥ tt ::ᵥ vector.nil),
  indices := c }

def mk3unique (c: vector ℕ 3) : gatenode :=
{ valence := 3,
  possib := [
    ff ::ᵥ ff ::ᵥ tt ::ᵥ vector.nil,
    ff ::ᵥ tt ::ᵥ ff ::ᵥ vector.nil,
    tt ::ᵥ ff ::ᵥ ff ::ᵥ vector.nil
  ],
  state := (ff, ff ::ᵥ  ff ::ᵥ  tt ::ᵥ vector.nil),
  indices := c }

structure satnet :=
(bts : list bitnode) (gts : list gatenode)
(nextbits nextgates : list ℕ) (table : list ℕ × list (list bool))
(tablesequence : list (list ℕ × list (list bool)))

def solv1 (s : satnet) : satnet :=
{ bts := s.bts,
  gts := s.gts,
  nextbits :=
    if s.bts.any bitnode.isconstant then
      (s.bts.enum.filter (λx:_×bitnode, x.2.isconstant)).map prod.fst
    else [0],
  nextgates := s.nextgates,
  table := s.table,
  tablesequence := [] }

[Mario Carneiro]

I don't know how to make sense of the definition of set in solv2; the list.map and list.foldr calls don't have enough arguments

[Mario Carneiro]

you should definitely break this down into bite sized pieces and ask questions one at a time

[Jared green]

i changed the set to this

let set:list ℕ := list.erase_dup
  ( list.foldr list.append (
          list.map prod.fst ∘ bitnode.indices
          (
            list.filter (λx,( ¬ (bitnode.considered x) = tt))
            (
              list.map
              (λx,(
                list.nth_le s.bts x (dec_trivial)
              ))
              s.nextbits
            )
          )
        )
    )

[Jared green]

subtype.val is the underlying function of what?

[Mario Carneiro]

If I replace the dec_trivial with sorry it still does not type check, bitnode.indices doesn't have the right type

[Mario Carneiro]

do you want it to be list.map (prod.fst ∘ bitnode.indices) ...?

[Mario Carneiro]

that also doesn't work

[Mario Carneiro]

Can you say in words what you are trying to express?

[Jared green]

the pointers to the gatenodes that are connected to the bitnodes that nextbits points to.

[Mario Carneiro]

and the foldr is still missing an argument; it takes 3 arguments, the function to fold, the initial value and the list. You have no initial value

[Mario Carneiro]

what does points to mean here?

[Mario Carneiro]

what should happen if s.nextbits contains an index out of range of s.bts?

[Mario Carneiro]

one easy thing to do is filter those indices out, so you get s.nextbits.filter_map (list.nth s.bts)

[Jared green]

the starting value is []

[Jared green]

the pointers are the indexes in the corresponding list where the connected node is at

[Mario Carneiro]

still not sure where you want to go with that list.map prod.fst ∘ bitnode.indices part

[Jared green]

if a function like vetnet is used as a refinement to satnet, the indices should not be out of range.

[Mario Carneiro]

So s.nextbits.filter_map (list.nth s.bts) is the collection of bitnodes pointed to by nextbits. where do considered and indices come up?

[Mario Carneiro]

Sure, but the types don't say that so you have to decide what to do anyway

[Mario Carneiro]

filter_map is an easy way to dodge the issue with nth_le

[Mario Carneiro]

Alternatively, you can give an instance of inhabited bitset and then you can use list.inth

[Jared green]

the second of the ordered pairs that bitnode.indices uses connects to a particular line of a gatenode

[Mario Carneiro]

aha, I think you want this:

let set : list ℕ :=
  (((s.nextbits.filter_map (list.nth s.bts))
    .filter (λx, ¬ bitnode.considered x))
    .bind (λ x:bitnode, x.indices.map prod.fst))
    .erase_dup

[Jared green]

i prefer to use filter_map

[Mario Carneiro]

Here's a way to write it monadically:

let set : list ℕ := list.erase_dup $ do
  n ← s.nextbits,
  x ← (list.nth s.bts n).to_list,
  guard (¬ bitnode.considered x),
  i ← x.indices,
  pure i.1

[Jared green]

does it matter?

[Mario Carneiro]

what do you mean?

[Mario Carneiro]

It's a matter of taste

[Jared green]

what would inform the choice to instead use the monadic version?

[Mario Carneiro]

it's a bit easier to write and maintain

[Jared green]

easier to understand?

[Mario Carneiro]

Both of the last two versions I wrote are okay for understanding, but normally you wouldn't be writing all these lists explicitly and instead you would describe things more declaratively, by describing the property that should hold about the values and letting lean figure out how to compute it

[Mario Carneiro]

it still looks too much like haskell code atm

[Jared green]

anyway i used the former

[Jared green]

what looks too much like haskell?

[Mario Carneiro]

Maybe it might help to start at the beginning, with the problem modeling. What are bitnode and gatenode, and how do the fields accomplish what they need to do?

[Mario Carneiro]

I suspect there are a number of missing propositional fields

[Patrick Massot]

Where does this idea of having all those lines with only parentheses come from?

[Jared green]

the entire network is composed of nodes representing bits and logic gates. a bit can be connected to the lines of any number of gates, while each line of a gate can only be connected to one bit. possib is an exhaustive enumeration of the ways the bits a gate is connected to can take on values. the algorithm that i was going for moves a front of consideration across the network, and bitnode.considered and gatenode.state.fst indicate that the node has been passed by.

[Mario Carneiro]

that sounds like bitnode.considered should not be a part of bitnode then

[Mario Carneiro]

What is the data required to define a network?

[Mario Carneiro]

What is the input and output of the algorithm?

[Jared green]

all the perentheses are necessary to tell what branch of the function graph you are looking at. it also help lean call on the antire value rather than the function that produced it.

[Mario Carneiro]

I think patrick is referring to the formatting of the parentheses, not their presence

[Jared green]

bitnode.considered is required for efficiency.

[Mario Carneiro]

efficiency in what sense?

[Jared green]

the formatting helps me personally to read what is there.

[Mario Carneiro]

I mean to say that your considered data should be separate from the network, since it's not part of the input

[Jared green]

it is linked to the bitnode by necessity.

[Mario Carneiro]

it can be layered over the bitnode just as well, thanks to dependent types

[Mario Carneiro]

but maybe that's getting ahead of ourselves. What are the other fields in bitnode? What do you mean by a "bit"? Is this like an internal wire in a logic gate diagram, or an external wire?

[Jared green]

the former.

[Mario Carneiro]

It seems like the network (the graph) should be separate from the space of states of the network (assignments of {0, 1} to the wires), but the current form doesn't seem to make a distinction

[Jared green]

why?

[Mario Carneiro]

Otherwise you can't talk about properties of networks, only properties of states. For example an unstable network (i.e. one with no valid assignment) can't be expressed

[Mario Carneiro]

Same as how formulas and assignments are distinguished in SAT

[Jared green]

an example, please.

[Jared green]

the way satnet is formulated, one does not necessarily have an output.

[Mario Carneiro]

I'm thinking of something like this for defining a network:

structure network :=
(bits gates : Type)
(valence : gates → ℕ)
(valuation : ∀ g : gates, vector bool (valence g) → bool)
(input : ∀ g : gates, vector bits (valence g))
(output : gates → bits → Prop)

def mknot : network :=
{ bits := bool,
  gates := unit,
  valence := λ _, 1,
  valuation := λ _ v, bnot (v.get 0),
  input := λ _, ff ::ᵥ vector.nil,
  output := λ _ b, b = tt }

[Jared green]

if there were equivalent functions (to all the ones being used) that can operate on those fields, then that would work.

[Mario Carneiro]

And an assignment would look like this:

structure assignment (n : network) :=
(value : n.bits → bool)
(valid : ∀ g b, n.output g b → n.valuation g ((n.input g).map value) = value b)

[Jared green]

but the reason i use lists is that such an implementation lends itself to optimization.

[Mario Carneiro]

This is for the abstract theory, where the lists get in the way. Once you have proofs about the abstract theory, the algorithm can be a refinement of it using lists and working in a special case where everything is finite and decidable

[Jared green]

fine.

[Mario Carneiro]

In fact, you will find that vector is not used much in mathlib, and there is some syntax sugar for fin n -> A style lists

[Mario Carneiro]

I think it is in data.matrix.notation, you can write ![a, b, c] to get a fin 3 -> A

[Jared green]

the reason i used vector was so that certain lists would have the same length.

[Mario Carneiro]

It looks like this:

import data.matrix.notation

structure network :=
(bits gates : Type)
(valence : gates → ℕ)
(valuation : ∀ g : gates, (fin (valence g) → bool) → bool)
(input : ∀ g : gates, fin (valence g) → bits)
(output : gates → bits → Prop)

def mknot : network :=
{ bits := bool,
  gates := unit,
  valence := λ _, 1,
  valuation := λ _ v, bnot (v 0),
  input := λ _, ![ff],
  output := λ _ b, b = tt }

structure assignment (n : network) :=
(value : n.bits → bool)
(valid : ∀ g b, n.output g b → n.valuation g (λ i, value (n.input g i)) = value b)

[Mario Carneiro]

fin n -> A is also fixed length lists, but you can compose them easier than lists, just using function composition

[Jared green]

what is fin n?

[Mario Carneiro]

it is the set of natural numbers less than n

[Mario Carneiro]

it's the canonical type with n elements

[Jared green]

ok

[Mario Carneiro]

What is satnet supposed to be?

[Jared green]

'satnet' is the type of a network of bitnodes and gatenodes. the name is due to the fact that any SAT instance can be used to build one.

[Jared green]

*and vice versa

[Mario Carneiro]

Here's a network which contains every SAT network as a sub-DAG:

namespace SAT
section
parameters (V : Type)

inductive formula
| var : V → formula
| true : formula
| and : formula → formula → formula
| not : formula → formula

inductive gate
| true : gate
| and : formula → formula → gate
| not : formula → gate

protected def valence : gate → ℕ
| gate.true := 0
| (gate.and _ _) := 2
| (gate.not _) := 1

protected def valuation : ∀ g : gate, (fin (valence g) → bool) → bool
| gate.true v := tt
| (gate.and _ _) (v:fin 2 → bool) := v 0 && v 1
| (gate.not _) (v:fin 1 → bool) := bnot (v 0)

protected def input : ∀ g : gate, fin (valence g) → formula
| gate.true := ![]
| (gate.and a b) := ![a, b]
| (gate.not a) := ![a]

inductive output : gate → formula → Prop
| true : output gate.true formula.true
| and (a b) : output (gate.and a b) (formula.and a b)
| not (a) : output (gate.not a) (formula.not a)

protected def network : network :=
{ bits := formula,
  gates := gate,
  valence := valence,
  valuation := valuation,
  input := input,
  output := output }

protected def eval (f : V → bool) : formula → bool
| (formula.var v) := f v
| formula.true := tt
| (formula.and a b) := eval a && eval b
| (formula.not a) := bnot (eval a)

protected def assignment (f : V → bool) : assignment network :=
{ value := eval f,
  valid := λ g b out, by cases out; refl }

end
end SAT

[Jared green]

what purpose does this serve?

[Jared green]

it might help to know what the algorithm does.
what is does is construct a sequence of truth tables, related to subsets of the gates, such that
each subset and the next intersects
each subset contains one gate that all the previous ones did not
each table is maximal for the set it represents and compatible with the previous one, while the choice of which gate is used minimizes the size of the table
and all the subsets together cover the entire network.
this process generates the information to certify satisfiability
then an entry in the last table is chosen, then in each previous one an entry compatible with the successive table is also chosen.
this is how a particular solution is generated.

[Jared green]

the lack of directionality specifically allows for information to traverse the network in all directions, so each gate is like 'if the lines are not in an allowed state then the network's valuations are invalid'