The queries h₀ and ∃x y, R(x) ∧ S(x, y)

Lax794877.Queries · concepts/Lax794877/Queries.lean · lax-794877

definition

Loading review…

Natural Language Statement

Definition

The schema has a unary relation $R$ , a binary relation $S$ , and a unary relation $T$ . The query $h_0 = \exists x\, y,\ R(x) \wedge S(x, y) \wedge T(y)$ is the smallest query whose probability is hard to compute, after Dalvi and Suciu; the query $\exists x\, y,\ R(x) \wedge S(x, y)$ is hierarchical, on the easy side of their dichotomy.

Concept map

1 concept; 8 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Tactic.FinCases
2	import Mathlib.Data.Fintype.BigOperators
3	import Mathlib.Order.Lattice.Nat
4	import Mathlib.Data.Set.Card
5	import Mathlib.ModelTheory.Order
6	import Mathlib.ModelTheory.Semantics
7	import Mathlib.ModelTheory.Complexity
8	import Mathlib.Order.PiLex
9	import Mathlib.Data.Prod.Lex
10	import Mathlib.Data.Fintype.EquivFin
11	import Mathlib.Logic.Equiv.Fin.Basic
12	import Mathlib.Data.Finite.Sigma
13	import Mathlib.Data.Fintype.Lattice
14	import Mathlib.Data.Fintype.Pigeonhole
15	import Mathlib.Dynamics.FixedPoints.Basic
16	import Mathlib.Algebra.BigOperators.Finprod
17	import Mathlib.Algebra.Order.BigOperators.Group.Finset
18	import Mathlib.ModelTheory.Syntax
19	import Mathlib.Data.Fintype.Card
20	import Mathlib.SetTheory.Cardinal.Finite
21	import Mathlib.Data.Finset.Max
22	import Mathlib.Logic.Equiv.Prod
23	import Mathlib.Algebra.BigOperators.Group.Finset.Basic
24	import Mathlib.Algebra.BigOperators.Pi
25	import Mathlib.Algebra.BigOperators.Ring.Finset
26	import Mathlib.Algebra.BigOperators.Field
27	import Mathlib.Algebra.Order.BigOperators.Ring.Finset
28	import Mathlib.Algebra.Order.Ring.Rat
29	import Mathlib.Algebra.Order.Field.Basic
30	import Mathlib.Data.Fintype.Pi
31	import Mathlib.Tactic.Linarith
32	import Mathlib.Tactic.FieldSimp
33	import Mathlib.Tactic.Ring
34	import Mathlib.Data.Set.Finite.Lemmas
35	import Mathlib.Algebra.Group.Action.Defs
36	import Mathlib.ModelTheory.Graph
37	import Mathlib.Data.Fintype.Sort
38	import Mathlib.Order.Hom.Set
39	import Mathlib.Algebra.BigOperators.Fin
40	import Mathlib.Data.Nat.Bitwise
41
42	/-!
43	---
44	title: The queries h₀ and ∃x y, R(x) ∧ S(x, y)
45	type: definition
46	---
47	The schema has a unary relation $R$ , a binary relation $S$ , and a unary
48	relation $T$ . The query $h_0 = \exists x\, y,\ R(x) \wedge S(x, y) \wedge T(y)$
49	is the smallest query whose probability is hard to compute, after
50	Dalvi and Suciu; the query $\exists x\, y,\ R(x) \wedge S(x, y)$ is
51	hierarchical, on the easy side of their dichotomy.
52	-/
53
54	namespace Lax794877.Queries
55
56	open FirstOrder
57
58	open FirstOrder.Language
59
60	/-- The relation symbols of the language. -/
61	inductive rstRel : ℕ → Type where
62	/-- `r a`. -/
63	\| r : rstRel 1
64	/-- `s a b`. -/
65	\| s : rstRel 2
66	/-- `t b`. -/
67	\| t : rstRel 1
68	deriving DecidableEq
69
70	/-- The schema of the example: two unary relations and a binary one. -/
71	def rst : FirstOrder.Language :=
72	⟨fun _ => Empty, rstRel⟩
73
74	instance instIsRelationalRst : FirstOrder.Language.IsRelational rst := fun _ =>
75	(inferInstance : IsEmpty Empty)
76
77	/-- `r a`. -/
78	abbrev rstR : rst.Relations 1 :=
79	.r
80
81	/-- `s a b`. -/
82	abbrev rstS : rst.Relations 2 :=
83	.s
84
85	/-- `t b`. -/
86	abbrev rstT : rst.Relations 1 :=
87	.t
88
89	open FirstOrder
90
91	open Language Structure
92
93	instance instFiniteSigmaNatRelationsRst : Finite (Σ n, rst.Relations n) :=
94	Finite.of_surjective
95	(fun i : Fin 3 => match i with
96	\| 0 => (⟨1, rstR⟩ : Σ n, rst.Relations n)
97	\| 1 => ⟨2, rstS⟩
98	\| 2 => ⟨1, rstT⟩)
99	(by
100	rintro ⟨n, R⟩
101	cases R
102	· exact ⟨0, rfl⟩
103	· exact ⟨1, rfl⟩
104	· exact ⟨2, rfl⟩)
105
106	/-- The query `h₀ = ∃ x y, R(x) ∧ S(x, y) ∧ T(y)`. -/
107	noncomputable def h0 : rst.Sentence :=
108	FirstOrder.Language.Formula.iExs (Fin 2)
109	(FirstOrder.Language.Relations.formula₁ rstR (FirstOrder.Language.Term.var (Sum.inr 0)) ⊓
110	(FirstOrder.Language.Relations.formula₂ rstS (FirstOrder.Language.Term.var (Sum.inr 0))
111	(FirstOrder.Language.Term.var (Sum.inr 1)) ⊓
112	FirstOrder.Language.Relations.formula₁ rstT (FirstOrder.Language.Term.var (Sum.inr 1))))
113
114	/-- The query `∃ x y, R(x) ∧ S(x, y)`. -/
115	noncomputable def rs : rst.Sentence :=
116	FirstOrder.Language.Formula.iExs (Fin 2)
117	(FirstOrder.Language.Relations.formula₁ rstR (FirstOrder.Language.Term.var (Sum.inr 0)) ⊓
118	FirstOrder.Language.Relations.formula₂ rstS (FirstOrder.Language.Term.var (Sum.inr 0))
119	(FirstOrder.Language.Term.var (Sum.inr 1)))
120
121	end Lax794877.Queries
122

Builds on

none

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

The queries h₀ and ∃x y, R(x) ∧ S(x, y)

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments