Writing a decidability instance

Stream: new members

[Nick Pilotti]

Hello, I have another question on the model theory project I am working on. I have defined the notion of truth in a structure and I am trying to write a decidable instance for certain cases. For example, I want a formula with just equality to be decidable if the equality relation in the universe the structure maps to is decidable, I want an and formula to be decidable if each of the component formulas are decidable, etc. I tried to figure this out for a while but I am stuck on the first case. Can someone help me with writing an instance of decidabile?

import algebra.group_power

structure language :=
(functions : ℕ → Type) (relations : ℕ → Type)

variable L : language

inductive term
| var           : ℕ → term
| func {n : ℕ}  : L.functions n → (fin n → term) → term

inductive formula
| eq          : term L → term L → formula
| rel {n : ℕ} : L.relations n → (fin n → term L) → formula
| neg         : formula → formula
| or          : formula → formula → formula
| all         : ℕ → formula → formula

notation ` v `    := term.var
notation ` v₀ `   := term.var 0
notation ` v₁ `   := term.var 1
notation ` v₂ `   := term.var 2

infix ` ≃ `:88   := formula.eq
prefix ` ∼ `:100 := formula.neg
infix  ` or `:50  := formula.or

open term
open formula

variables (A : Type*) (iA : inhabited A)

/-- Def 1.6.1. An L-structure -/
structure Structure [inhabited A] :=
(functions : Π {n : ℕ}, L.functions n → (fin n → A) → A)
(relations : Π {n : ℕ}, L.relations n → (fin n → A) → Prop)

variable 𝔸 : Structure L A

/-- Variable assignment function into A -/
def var_assign := ℕ → A

/-- x-modification of the assignment function s -/
def modification_of (s : var_assign A) (x : ℕ) (a : A) : var_assign A :=
  λ (n : ℕ), if n = x then a else s n

notation s `[`x`|`a`]` := modification_of _ s x a

/-- Term assignment function -/
def term_assign := term L → A

/-- The term assignment function induced by s -/
def term_assign_of_s (s : var_assign A) : term_assign L A
| (v n)                 := s n
| (func fsymb args)     := 𝔸.functions fsymb (λ n, term_assign_of_s (args n))

notation ` * ` := term_assign_of_s _ _ _

/-- A structure 𝔸 satifies formula φ with assignment s -/
def satisfies_with_assignment : var_assign A → formula L → Prop
  | s (t₁ ≃ t₂)           := (* 𝔸 s) t₁ = (* 𝔸 s) t₂
  | s (rel rsymb args)    := 𝔸.relations rsymb (λ n, (* 𝔸 s) (args n))
  | s ∼φ₁                 := ¬(satisfies_with_assignment s φ₁)
  | s (φ₁ or φ₂)          := (satisfies_with_assignment s φ₁) ∨ (satisfies_with_assignment s φ₂)
  | s (all n φ₁)          := ∀ a : A, satisfies_with_assignment (s[n|a]) φ₁

notation 𝔸` ⊨ `φ`[`s`]` := satisfies_with_assignment _ _ _ 𝔸 s φ

variables (s : var_assign A)

-- How to write a deciable instance?
instance [decidable_eq A] : decidable (satisfies_with_assignment _ _ _ 𝔸 s (v₀ ≃ v₁)) := sorry

[Alex J. Best]

In this case, simply

instance [decidable_eq A] : decidable (satisfies_with_assignment _ _ _ 𝔸 s (v₀ ≃ v₁)) := begin
rw satisfies_with_assignment,
apply_instance,
end

works

[Nick Pilotti]

Thanks!

[Nick Pilotti]

How would I handle the other cases? For example the not case

[Nick Pilotti]

Specifically I'm not sure where the place the decidable instance for φ

notation 𝔸` ⊨ `φ` | `s:= satisfies_with_assignment _ _ _ 𝔸 s φ

variables (s : var_assign A)

instance [decidable_eq A] : ∀ n m : ℕ, decidable (𝔸 ⊨ (v n ≃ v m) | s) := begin
intros n m,
rw satisfies_with_assignment,
apply_instance,
end

instance : ∀ [decidable φ] φ : formula L , decidable (𝔸 ⊨ ∼φ | s) := begin
rw satisfies_with_assignment,
apply_instance
end

[Alex J. Best]

Is this what you are looking for

notation 𝔸` ⊨ `φ` | `s:= satisfies_with_assignment _ _ _ 𝔸 s φ

variables (s : var_assign A)

instance eq_decidable [decidable_eq A] : ∀ n m : ℕ, decidable (𝔸 ⊨ (v n ≃ v m) | s) := begin
intros n m,
rw satisfies_with_assignment,
apply_instance,
end

instance not_decidable {φ : formula L} [decidable (𝔸 ⊨ φ | s)] : decidable (𝔸 ⊨ ∼φ | s) := begin
rw satisfies_with_assignment,
apply_instance
end

I don't really know the mathematical background of what you are trying to do so I'm not sure if this is what you want for your application

[Nick Pilotti]

Yes that's perfect thank you

[Nick Pilotti]

Another question I am having, I want to type #eval so that I can view the proposition that gets computed by satisfies_with_assignment, but Lean says that the result doesn't have an instance of has_repr. How can I use #eval to see the Prop that gets computed?

[Yaël Dillies]

Give it an docs#has_repr instance!

[Yaël Dillies]

The problem here is that you haven't told Lean how to print your terms. So tell Lean that and it will happily comply.

[Bryan Gin-ge Chen]

I don't think you'll be able to provide a useful instance. (whoops, ignore that) See this related thread.

[Yaël Dillies]

I think you're wrong on that one, Bryan.

[Bryan Gin-ge Chen]

Yeah, I misread. Sorry!

[Yaël Dillies]

Sure we can't get a useful has_repr on satisfies_with_assignment, but we can define satisfies_with_assignment_string that does the same but "with words".

[Yaël Dillies]

Bryan Gin-ge Chen said:

Yeah, I misread. Sorry!

Oh wait what are you refering to? The thread you pointed to seems pretty relevant.

[Bryan Gin-ge Chen]

I was only referring to my claim "I don't think you'll be able to provide a useful instance."

[Nick Pilotti]

I'm not sure I'm understanding completely. From that thread what I've gathered is that I can't write a has_repr instance for Prop because it is a Sort? But I could write satisfies_with_assignment_string that would do what exactly?

[Yakov Pechersky]

I think you want #reduce and not #eval

[Nick Pilotti]

Yes, reduce did what I was looking for!

[Antoine Chambert-Loir]

Nick Pilotti said:

Another question I am having, I want to type #eval so that I can view the proposition that gets computed by satisfies_with_assignment, but Lean says that the result doesn't have an instance of has_repr. How can I use #eval to see the Prop that gets computed?

I am precisely asking myself the same question today! Did you get an answer?

[Kyle Miller]

@Antoine Chambert-Loir Props don't get computed, so there's nothing to print out with #eval (the link above to the related thread mentions how the VM represents them as 0). Are you able to use #reduce?

[Antoine Chambert-Loir]

Kyle Miller said:

Antoine Chambert-Loir Props don't get computed, so there's nothing to print out with #eval (the link above to the related thread mentions how the VM represents them as 0). Are you able to use #reduce?

Yes, but it says nothing about the “truth value” of the Prop. I didn't find a conversion to bool but this works:

-- prints 0
#reduce ite (list.sorted (λ (a b : ℕ), (a<b)) [1,12,5,29]) (1) (0)
-- prints 1
#reduce ite (list.sorted (λ (a b : ℕ), (a<b)) [1,2,5,29]) (1) (0)

[Antoine Chambert-Loir]

By the way, it seems that Lean can pretty much compute by itself the valididity of such an expression. How can one make use of this ability in a proof, without having to resort to a simp that uses of a lot bit1_lt_bit1 and so on… ?

[Johan Commelin]

Is dec_trivial what you want?

[Johan Commelin]

(Note that (λ (a b : ℕ), (a<b)) can also be written as (<).)

[Johan Commelin]

What I mean is that

example : list.sorted (λ (a b : ℕ), (a<b)) [1,2,5,29] := dec_trivial

should hopefully "just work"

[Kevin Buzzard]

I didn't find a conversion to bool

Let Goedel know when you do!

[Kyle Miller]

The way you do the conversion to bool is a plain coercion:

#eval (list.sorted (λ (a b : ℕ), (a<b)) [1,12,5,29] : bool)

#eval (list.sorted (λ (a b : ℕ), (a<b)) [1,2,5,29] : bool)

(This is using decidable instances.)

[Johan Commelin]

I just checked, and

example : list.sorted (<) [1,2,5,29] := dec_trivial

does indeed work

[Antoine Chambert-Loir]

Kevin Buzzard said:

I didn't find a conversion to bool

Let Goedel know when you do!

OK, then there must be something I don't understand about Prop in Lean. Prop.fintype says there are only two possible Props, true and false, so…

[Eric Wieser]

Ah, but docs#Prop.fintype is noncomputable! doesn't tell you how to check whether the prop you have is the true one or the false one. It's just a restatement of docs#classical.em

[Kyle Miller]

Antoine Chambert-Loir said:

OK, then there must be something I don't understand about Prop in Lean. Prop.fintype says there are only two possible Props, true and false, so…

So why do we bother writing proofs? :smile:

[Antoine Chambert-Loir]

OK, now I understand what you meant this morning.
In my case, I was working with lists, and it is clear that the definition of list.sorted corresponds to an algorithm. If the list is explicitly filled with explicit elements, what I expect is probably a tactic that automatically fills in the details.

[Kevin Buzzard]

dec_trivial runs the algorithm

[Ali Alamen]

when I started working on Lean proof assistant on visual studio code, I have followed the instructions on Lean webstie but after all of tips the lean Infoviewer didn't show any thing just "Waiting for Lean server to start..." where is the problem Capture.PNG