# data[].attributes.body
O objetivo é traduzir as regras de derivação da dedução natural em teoremas do Coq e depois prová-los.

Em anexo alguns exemplos.

# data[].attributes.attachment_link.title
Join the Grupo de Lógica Discord Server!

# data[].attributes.attachment_link.description
Check out the Grupo de Lógica community on Discord - hang out with 8 other members and enjoy free voice and text chat.

# data[].attributes.attachment_link.readable_text
Meet doesn't work on your browser

To join the video meeting

Visit meet.google.com in Google Chrome, Mozilla Firefox, or Microsoft Edge

To install and use Meet on a mobile device, go to

or the

# data[].attributes.attachment_link.description
Meet doesn't work on your browser To join the video meeting Visit meet.google.com in Google Chrome, Mozilla Firefox, or Microsoft Edge To install and use Meet on a mobile device, go to or the

# data[].attributes.attachment_link.title
GitHub - renatoleme/Grupo_Coq: Repositório do grupo de estudos Coq.

# data[].attributes.attachment_link.description
Repositório do grupo de estudos Coq. Contribute to renatoleme/Grupo_Coq development by creating an account on GitHub.

# data[].attributes.body
Definition less_than_two (l : list nat) :=
match l with
| h1::h2::tl => h1 <=? h2
| _ => true
end.

Definition leq2 (l : list nat) :=
  match l with
    | nil => true
    | a::nil => true
    | a::b::x => a <=? b
  end.

# data[].attributes.body
Provar

Theorem sorted_Equiv : forall l, is_sorted l = is_sorted2 l.

onde

Fixpoint is_sorted (l: list nat) :=
match l with
| a::b::tail => andb (leq2 (a::b::nil)) (is_sorted tail)
| _ => true
end.

e

Fixpoint is_sorted2 (l : list nat) :=
match l with
| nil => true
| h::tl =>
    if less_than_two l then is_sorted tl
    else false
end.