Homework Help is Here – Start Your Trial Now!
Engineering
Computer Science
File Edit View Navigation Templates Queries Tools Compile Debug Windows Help projectfianl ex_02_sumlist Require Import Coq.Lists. List. Import ListNotations. Section LinkedList. Variable A: Type. Inductive LinkedList = LNil LCons (x: A) (xs LinkedList). End LinkedList. Section Append. Fixpoint append (xs ys: LinkedList) : LinkedList := match xs with LNil => ys | LCons x xs' => LCons x (append xs' ys) end. End Append. From iris.base_logic Require Import invariants. From iris.proofmode Require Import tactics. Section AppendProof. Context inG E (authR (listUR A))). Lemma append_nil_r (xs: LinkedList) Proof. induction xs; simpl; auto. Qed. append xs LNil xs. Lemma append_assoc (xs ys zs LinkedList) : append (append xs ys) zs = append xs (append ys zs). Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_comm (xs ys: LinkedList) : append xs ys = append ys xs. Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_cons_r (x: A) (xs ys: LinkedList) : append xs (LCons x ys) = LCons x (append xs ys). Proof. induction xs: simpl: auto. Messages Errors Jobs The term "LinkedList" has type "Type -> Type" which should be Set, Prop or Type.

File Edit View Navigation Templates Queries Tools Compile Debug Windows Help projectfianl ex_02_sumlist Require Import Coq.Lists. List. Import ListNotations. Section LinkedList. Variable A: Type. Inductive LinkedList = LNil LCons (x: A) (xs LinkedList). End LinkedList. Section Append. Fixpoint append (xs ys: LinkedList) : LinkedList := match xs with LNil => ys | LCons x xs' => LCons x (append xs' ys) end. End Append. From iris.base_logic Require Import invariants. From iris.proofmode Require Import tactics. Section AppendProof. Context inG E (authR (listUR A))). Lemma append_nil_r (xs: LinkedList) Proof. induction xs; simpl; auto. Qed. append xs LNil xs. Lemma append_assoc (xs ys zs LinkedList) : append (append xs ys) zs = append xs (append ys zs). Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_comm (xs ys: LinkedList) : append xs ys = append ys xs. Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_cons_r (x: A) (xs ys: LinkedList) : append xs (LCons x ys) = LCons x (append xs ys). Proof. induction xs: simpl: auto. Messages Errors Jobs The term "LinkedList" has type "Type -> Type" which should be Set, Prop or Type.

New Perspectives on HTML5, CSS3, and JavaScript
New Perspectives on HTML5, CSS3, and JavaScript
6th Edition
ISBN:9781305503922
Author:Patrick M. Carey
Publisher:Patrick M. Carey
Chapter12: Working With Document Nodes And Style Sheets: Creating A Dynamic Document Outline
Section12.1: Visual Overview: Exploring The Node Tree
Problem 5QC
See similar textbooks
icon
Related questions
Question

Can you Fix this error in the following image 

Require Import Coq.Lists.List.
Import ListNotations.

Section LinkedList.

  Variable A : Type.

  Inductive LinkedList :=
  | LNil
  | LCons (x : A) (xs : LinkedList).

End LinkedList.

Section Append.

  Fixpoint append (xs ys : LinkedList) : LinkedList :=
    match xs with
    | LNil => ys
    | LCons x xs' => LCons x (append xs' ys)
    end.

End Append.

From iris.base_logic Require Import invariants.
From iris.proofmode Require Import tactics.

Section AppendProof.

  Context `{!inG Σ (authR (listUR A))}.

  Lemma append_nil_r (xs : LinkedList) : append xs LNil = xs.
  Proof.
    induction xs; simpl; auto.
  Qed.

  Lemma append_assoc (xs ys zs : LinkedList) :
    append (append xs ys) zs = append xs (append ys zs).
  Proof.
    induction xs; simpl; auto.
    rewrite IHxs. reflexivity.
  Qed.

  Lemma append_comm (xs ys : LinkedList) :
    append xs ys = append ys xs.
  Proof.
    induction xs; simpl; auto.
    rewrite IHxs. reflexivity.
  Qed.

  Lemma append_cons_r (x : A) (xs ys : LinkedList) :
    append xs (LCons x ys) = LCons x (append xs ys).
  Proof.
    induction xs; simpl; auto.
  Qed.

End AppendProof.



File Edit View Navigation Templates Queries Tools Compile Debug Windows Help projectfianl ex_02_sumlist Require Import Coq.Lists. List. Import ListNotations. Section LinkedList. Variable A: Type. Inductive LinkedList = LNil LCons (x: A) (xs LinkedList). End LinkedList. Section Append. Fixpoint append (xs ys: LinkedList) : LinkedList := match xs with LNil => ys | LCons x xs' => LCons x (append xs' ys) end. End Append. From iris.base_logic Require Import invariants. From iris.proofmode Require Import tactics. Section AppendProof. Context inG E (authR (listUR A))). Lemma append_nil_r (xs: LinkedList) Proof. induction xs; simpl; auto. Qed. append xs LNil xs. Lemma append_assoc (xs ys zs LinkedList) : append (append xs ys) zs = append xs (append ys zs). Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_comm (xs ys: LinkedList) : append xs ys = append ys xs. Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_cons_r (x: A) (xs ys: LinkedList) : append xs (LCons x ys) = LCons x (append xs ys). Proof. induction xs: simpl: auto. Messages Errors Jobs The term "LinkedList" has type "Type -> Type" which should be Set, Prop or Type.
Transcribed Image Text:File Edit View Navigation Templates Queries Tools Compile Debug Windows Help projectfianl ex_02_sumlist Require Import Coq.Lists. List. Import ListNotations. Section LinkedList. Variable A: Type. Inductive LinkedList = LNil LCons (x: A) (xs LinkedList). End LinkedList. Section Append. Fixpoint append (xs ys: LinkedList) : LinkedList := match xs with LNil => ys | LCons x xs' => LCons x (append xs' ys) end. End Append. From iris.base_logic Require Import invariants. From iris.proofmode Require Import tactics. Section AppendProof. Context inG E (authR (listUR A))). Lemma append_nil_r (xs: LinkedList) Proof. induction xs; simpl; auto. Qed. append xs LNil xs. Lemma append_assoc (xs ys zs LinkedList) : append (append xs ys) zs = append xs (append ys zs). Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_comm (xs ys: LinkedList) : append xs ys = append ys xs. Proof. induction xs; simpl; auto. rewrite IHxs. reflexivity. Qed. Lemma append_cons_r (x: A) (xs ys: LinkedList) : append xs (LCons x ys) = LCons x (append xs ys). Proof. induction xs: simpl: auto. Messages Errors Jobs The term "LinkedList" has type "Type -> Type" which should be Set, Prop or Type.
Expert Solution
steps

Step by step

Solved in 2 steps

SEE SOLUTIONCheck out a sample Q&A here
Blurred answer
Recommended textbooks for you
New Perspectives on HTML5, CSS3, and JavaScript
New Perspectives on HTML5, CSS3, and JavaScript
Computer Science
ISBN:
9781305503922
Author:
Patrick M. Carey
Publisher:
Cengage Learning
EBK JAVA PROGRAMMING
EBK JAVA PROGRAMMING
Computer Science
ISBN:
9781337671385
Author:
FARRELL
Publisher:
CENGAGE LEARNING - CONSIGNMENT
Systems Architecture
Systems Architecture
Computer Science
ISBN:
9781305080195
Author:
Stephen D. Burd
Publisher:
Cengage Learning
C++ Programming: From Problem Analysis to Program…
C++ Programming: From Problem Analysis to Program…
Computer Science
ISBN:
9781337102087
Author:
D. S. Malik
Publisher:
Cengage Learning
Programming with Microsoft Visual Basic 2017
Programming with Microsoft Visual Basic 2017
Computer Science
ISBN:
9781337102124
Author:
Diane Zak
Publisher:
Cengage Learning
Programming Logic & Design Comprehensive
Programming Logic & Design Comprehensive
Computer Science
ISBN:
9781337669405
Author:
FARRELL
Publisher:
Cengage
SEE MORE TEXTBOOKS