EEVblog Electronics Community Forum

General => General Technical Chat => Topic started by: vlad777 on June 21, 2017, 11:31:50 pm

Title: Anybody knows Coq?
Post by: vlad777 on June 21, 2017, 11:31:50 pm

I am trying to prove that if today is Friday then next day is weekend.

The last line fails , because I don't know the syntax , please help.

First on the list is to express in proper syntax what is on the last line,
the prove it.

BTW I am desperate for most most basic examples for Coq.

Many thanks.


Inductive day : Type :=
  | monday : day
  | tuesday : day
  | wednesday : day
  | thursday : day
  | friday : day
  | saturday : day
  | sunday : day.

Definition next_weekday (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => saturday
  | saturday => sunday
  | sunday => monday
  end.

Definition is_weekend (d:day) : bool :=
  match d with
  | monday => false
  | tuesday => false
  | wednesday => false
  | thursday => false
  | friday => false
  | saturday => true
  | sunday => true
  end.



Theorem myt : (forall x : day, next_weekday(friday) -> is_weekend(x) ).

Title: Re: Anybody knows Coq?
Post by: vlad777 on June 22, 2017, 12:11:46 am

This works:

Theorem myt : forall (x : day) , is_weekend(next_weekday(friday)) =true .

But I would like a theorem that is not simultaneously the proof itself.

Edit:

This is better:

Theorem myt : forall (x : day) , is_weekend(x)=true  -> next_weekday(x)= monday \/ next_weekday(x)= sunday .

Now how do I prove it?


Edit2: This is what I meant:

Theorem myt : forall x : day, next_weekday(x)=sunday -> is_weekend(x)=true .