I have a question about the: Record and Definition
I have this definition:
Definition rule := term -> term.
and I write a boolean function for it.
Definition beq_rule a b := beq_term a && beq_term b.
where beq_term : term -> term -> bool.
so my definition of beq_rule actually return exactly type of beq_term which is not what I want here. I want it return for me a type: rule -> rule -> bool.
So I changed a definition of rule by Record:
Record rule := mkRule {lhs : term; rhs : term}.
and
Definition beq_rule (a b : rule) : bool :=
beq_term (lhs a) (lhs b) && beq_term (rhs a) (rhs b).
My question is that:
1) What is the different between my first defined rule used Definition and another used Record?
2) If I want to define rule by Definition can I give an alias lhs and rhs likes in Record definition?
Your two definitions of rule are saying totally different things
Definition rule := term -> term
is defining rule as a type (or Prop) alias of the function type term -> term. Hence
Definition not_what_you_meant : rule := fun t => t.
will happily compile.
As to the relation between Record and Definition. Record is just a macro that converts into an Inductive. So
Record rule := mkRule {lhs : term; rhs : term}.
is the same as
Inductive rule := mkRule : term -> term -> rule.
plus accessor functions
Definition lhs (r : rule) : term :=
match r with
mkRule l _ => l
end.
etc.
You should think of Inductive as being fundamentally different from Definition. Definition defines an alias. Another way f saying this is Definitions are "referentially transparent", you can (up to variable renaming) always substitute the right hand side of a definition for any occurrence of its name.
Inductive on the other hand defines type (elements of Coqs universes) by listing off a set of constructors. In more logical way of thinking, Inductive defines a logical proposition in terms of its elimination/introduction rules in a way that ensures "harmony".