yunoj / coq Goto Github PK

Machine: ubuntu 18.04
Running on: coqide
coq version: 8.9.0
installed with: opam

I have trouble starting on the second chapter induction.v.

Error: Cannot find a physical path bound to logical path matching suffix
<> and prefix LF.

This message is displayed after compilation. My _CoqProject file has one line "-Q . LF". My coqide's preferences points to _CoqProject as expected.

The line creating above error is: From LF Require Export Basics. (I have compiled Basics.v and have Basics.vo file in the same directory)

I have searched the internet and issued on coq github and still have no answer.

This may not be an appropriate question for you but this has been agonizing me for almost a week now. Hope you can help me on this problem.

Thank you in advance.

Last week has been midterm week in my school so I couldn't spend much time on studies that you told me to do. I am sorry about that.

I started studying lists in coq and got stuck on an example problem.

The example asks me to define fixpoint remove_all. Below is the given format.

Fixpoint remove_all (v:nat) (s:bag) : bag :=

this should remove all elements in s that is equal to v. (nat is abbreviation for natural number and bag is defined as natural number list)

Here is what I got so far:

Fixpoint remove_all (v:nat) (s:bag) : bag :=
  match s with 
  | nil => nil
  | h :: t => if eqb h v then t v t else match t with
              | nil => nil
              | h1 :: t1 => if eqb h1 v then h :: remove_all v t1 else h :: remove_all v t
              end
end.

My code first compares the head of the list with v and if they are not the same, it moves on and appends the tail with all elements equal to v removed. For example, if a list is constructed as [h; h1; t1], h is compared with v and if they are the same, [h1; t1] is returned. If they are not the same, h1 is compared with v, appending t with h --[h; t1]-- when same and moving on to testing the rest of the list when not.

The problem is when 5's are to be removed from [1; 2; 5; 5; 3], the resulting list will be [3] when it should be [1; 2; 3]. How can I concatenate the list with the one in the previous recursion?

Sorry for the long question.

Thank you in advance!

Defining Church numerals in the extra examples section of polymorphism chapter isn't working out as expected.

Below is give code:

Definition cnat := forall X : Type, (X -> X) -> X -> X.

Definition zero : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => x.

Definition one : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => f x.

Definition two : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => f (f x).

and this isn't that hard to understand. But I am asked to define successor(1 -> 2, 2->3, so on) and below is my code.

Definition succ (n : cnat) : cnat :=
  fun X f x => X f (f x).

The way I intended my definition to be read is "infer from the input cnat type, function and value and use the aforesaid attributes to yield f (f (x)) of type X." The problem is that I can't figure out how to take n into account. I guess this should work for Example succ_2 : succ one = two. but I am pretty sure that it will fail for other cases. Please help...

Hello professor,

I hope that you are having a good time with your family for 어린이날.

I have to interrupt you though for a problem with poly.v in coq.

It's about inductively defined types and here goes.

Inductive mumble : Type :=
  | a
  | b (x : mumble) (y : nat)
  | c.

Inductive grumble (X:Type) : Type :=
  | d (m : mumble)
  | e (x : X).

Above is the given code and I have to decide whether given statements are well-typed elements of [grumble X].

I did Check d bool (b a 5). and there was no error even though bool is another Type just like mumble and does not belong to mumble. What I understood from the reading materials is m in d (m : mumble) should belong to mumble. Since b a 5 is an element of mumble and bool is not, shouldn't the line be Check d (b a 5) to not raise an error?