Questions tagged [definition]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
5 votes
2 answers
257 views

Unclarity about Preorder class in Lean4

I realize the port of Mathlib to Lean4 is not finished yet, but I've run into a definition that I do not quite understand. I'm quite new at using theoremprovers as well as stackexchange, so please be ...
Pieter Cuijpers's user avatar
5 votes
0 answers
217 views

An algorithm for the substitution of formulas for predicates in first order logic

I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
user695931's user avatar
4 votes
2 answers
205 views

Coq defining a hierarchy of collections of integers with infinitely many "levels"

I'm trying to formalize a small part of higher-order arithmetic in Coq as an exercise (Wikipedia article for second-order arithmetic). It's straightforward to formalize something resembling second-...
Greg Nisbet's user avatar
  • 2,741
2 votes
1 answer
76 views

How do clausal definitions work?

I'm most familiar with the metatheory of calculi based around expressions. But systems like Agda use separate clauses for definitions. ...
Molly Stewart-Gallus's user avatar
2 votes
1 answer
65 views

Packaging Mathematical Structures in Coq: Help Understanding a Definition

Context I am a relatively new user to Coq with a decent understanding of the basics of dependent type theory and am midway through chapter 2 of the Software Foundations Series of books. I want to ...
user2628206's user avatar
2 votes
1 answer
135 views

Is there a way to rename parameters when including/reusing a module type in Coq?

Say I have a (more general) module type Collection that specifies some operations like read and write and now I want to create (more specialized) module types like <...
C.E.Sally's user avatar
  • 121
1 vote
2 answers
91 views

Defining a Recursive Function decreasing on one argument with < and another structurally

I want to define a function which decreases in one argument using < and on another structurally. What is the least painful way to do this? Among the many options (Function, Program Fixpoint, ...
Agnishom Chattopadhyay's user avatar
1 vote
1 answer
61 views

Question about default definitions in fields

In Unclarity about Preorder class in Lean4 I asked why the third and fourth field (lt and lt_iff_le_not_le) in the definition of MyPreorder below would both be necessary, as one follows from the other ...
Pieter Cuijpers's user avatar
0 votes
1 answer
80 views

Define a function using another function

I want to define a translation function g from another function f. Definition trans (f g : Q -> Q) (t : Q) := forall q : Q, f (q + t) == g q. In the above code,...
with-forest's user avatar