Construct a new record instances when the Record type has dependent binders in Coq
1
I intended to construct a new vector instance of Type Vector in the following code. However, initially, the Vector Record type has dependent ident binders. Like the second ident binder' or the second field -- 'proof' was dependent on the firstident binder' -- 'mpOf'. When I try to define the subtraction of two mass points, I find it impossible to pass the coq kernel.
Require Export Coq.Reals.Reals.
Open Scope R_scope.
Definition Point:= Type.
Record massPoint: Type := cons{number: R; point: Point}.
Definition isVector (v:massPoint) := exists A B : Point, v = add_MP(cons (-1) A)(cons 1 B).
Record Vector : Type := vecCons { mpOf : massPoint ; proof : isVector mpOf}.
Variable sub_MP: massPoint -> massPoint -> massPoint.
Definition point_sub (p1 p2: massPoint):Vector:=
vecCons (sub_MP p1 p2) proof (sub_MP p1 p2). (* errorsome definition*)
Anyone has any idea on how to define the point_sub?
record coq
edited Nov 25 '18 at 8:48
Robin Green
22.3k875155
asked Nov 25 '18 at 3:38
isPrimeisPrime
649
add a comment |
1
I intended to construct a new vector instance of Type Vector in the following code. However, initially, the Vector Record type has dependent ident binders. Like the second ident binder' or the second field -- 'proof' was dependent on the firstident binder' -- 'mpOf'. When I try to define the subtraction of two mass points, I find it impossible to pass the coq kernel.
Require Export Coq.Reals.Reals.
Open Scope R_scope.
Definition Point:= Type.
Record massPoint: Type := cons{number: R; point: Point}.
Definition isVector (v:massPoint) := exists A B : Point, v = add_MP(cons (-1) A)(cons 1 B).
Record Vector : Type := vecCons { mpOf : massPoint ; proof : isVector mpOf}.
Variable sub_MP: massPoint -> massPoint -> massPoint.
Definition point_sub (p1 p2: massPoint):Vector:=
vecCons (sub_MP p1 p2) proof (sub_MP p1 p2). (* errorsome definition*)
Anyone has any idea on how to define the point_sub?
record coq
edited Nov 25 '18 at 8:48
Robin Green
22.3k875155
asked Nov 25 '18 at 3:38
isPrimeisPrime
649
add a comment |
1
1
1
I intended to construct a new vector instance of Type Vector in the following code. However, initially, the Vector Record type has dependent ident binders. Like the second ident binder' or the second field -- 'proof' was dependent on the firstident binder' -- 'mpOf'. When I try to define the subtraction of two mass points, I find it impossible to pass the coq kernel.
Require Export Coq.Reals.Reals.
Open Scope R_scope.
Definition Point:= Type.
Record massPoint: Type := cons{number: R; point: Point}.
Definition isVector (v:massPoint) := exists A B : Point, v = add_MP(cons (-1) A)(cons 1 B).
Record Vector : Type := vecCons { mpOf : massPoint ; proof : isVector mpOf}.
Variable sub_MP: massPoint -> massPoint -> massPoint.
Definition point_sub (p1 p2: massPoint):Vector:=
vecCons (sub_MP p1 p2) proof (sub_MP p1 p2). (* errorsome definition*)
Anyone has any idea on how to define the point_sub?
record coq
edited Nov 25 '18 at 8:48
Robin Green
22.3k875155
asked Nov 25 '18 at 3:38
isPrimeisPrime
649
I intended to construct a new vector instance of Type Vector in the following code. However, initially, the Vector Record type has dependent ident binders. Like the second ident binder' or the second field -- 'proof' was dependent on the firstident binder' -- 'mpOf'. When I try to define the subtraction of two mass points, I find it impossible to pass the coq kernel.
Require Export Coq.Reals.Reals.
Open Scope R_scope.
Definition Point:= Type.
Record massPoint: Type := cons{number: R; point: Point}.
Definition isVector (v:massPoint) := exists A B : Point, v = add_MP(cons (-1) A)(cons 1 B).
Record Vector : Type := vecCons { mpOf : massPoint ; proof : isVector mpOf}.
Variable sub_MP: massPoint -> massPoint -> massPoint.
Definition point_sub (p1 p2: massPoint):Vector:=
vecCons (sub_MP p1 p2) proof (sub_MP p1 p2). (* errorsome definition*)
Anyone has any idea on how to define the point_sub?
record coq
record coq
edited Nov 25 '18 at 8:48
Robin Green
22.3k875155
asked Nov 25 '18 at 3:38
isPrimeisPrime
649
edited Nov 25 '18 at 8:48
Robin Green
22.3k875155
asked Nov 25 '18 at 3:38
isPrimeisPrime
649
edited Nov 25 '18 at 8:48
Robin Green
22.3k875155
edited Nov 25 '18 at 8:48
Robin Green
22.3k875155
edited Nov 25 '18 at 8:48
Robin Green
22.3k875155
22.3k875155
asked Nov 25 '18 at 3:38
isPrimeisPrime
649
asked Nov 25 '18 at 3:38
isPrimeisPrime
649
asked Nov 25 '18 at 3:38
isPrimeisPrime
649
649
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
2
You are having basic instantiation problems with regards on what a proof is. See for example this code and try to understand what you are missing:
Require Import Coq.Reals.Reals.
Open Scope R_scope.
Definition Point := Type.
Record massPoint: Type := cons { number: R; point: Point}.
Variable add_MP: massPoint -> massPoint -> massPoint.
Variable sub_MP: massPoint -> massPoint -> massPoint.
Definition isVector (v : massPoint) :=
exists A B : Point, v = add_MP (cons (-1) A) (cons 1 B).
Record Vector : Type := vecCons { mpOf : massPoint; proof : isVector mpOf }.
Definition point_sub (p1 p2: massPoint) : Vector.
Proof.
refine (vecCons (sub_MP p1 p2) _).
repeat eexists.
answered Nov 25 '18 at 3:59
ejgallegoejgallego
5,3641925
It looks like Coq cannot find the supporting mass point A and B. So I think it should beDefinition point_sub (p1 p2: massPoint) : Vector := vecCons (sub_MP p1 p2) add_MP (cons (-1) (point p1))(cons 1 (point p2)).But coq kernel is still complainingwhile it is expected to have type "isVector (sub_MP p1 p2)".I feel like I don't have enough commands in my proof repertoire to tackle it. Or I didn't understand your hint well enough. If possible, could you please elaborate a bit? Much appreciate your way of giving hints.
– isPrime
Nov 25 '18 at 4:46
You need to find ?A ?B such that ` sub_MP p1 p2 = add_MP {| number := -1; point := ?A |} {| number := 1; point := ?B |}` The way you write the above term doesn't make sense to the Coq typer, you are expected to write a term with the above type.
– ejgallego
Nov 25 '18 at 5:20
Honestly, the syntax is exactly the help I need. I can’t figure out how to write it in a way that Coq understands. I still lack the knowledge of it. If you decide to write it out, would you please also explain why the syntax is written that way? I want to understand the connections.
– isPrime
Nov 25 '18 at 15:31
You need to proveLemma my_proof : exists A B, sub_MP p1 p2 = add_MP {| number := -1; point := A |} {| number := 1; point := B |}, then you can usemy_proofin the construction of your record. But I'd say you need to take a course in Coq first, so you learn the basic syntax and typing rules first.
– ejgallego
Nov 25 '18 at 16:31
1
Thanks for the further hint. I'm able to construct that new record using the following syntaxDefinition mp_sub (p1 p2: massPoint) : Vector:= vecCons (sub_MP p1 p2) (mp_proof p1 p2).
– isPrime
Nov 25 '18 at 17:48
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
draft saved
draft discarded
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53464448%2fconstruct-a-new-record-instances-when-the-record-type-has-dependent-binders-in-c%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
2
You are having basic instantiation problems with regards on what a proof is. See for example this code and try to understand what you are missing:
Require Import Coq.Reals.Reals.
Open Scope R_scope.
Definition Point := Type.
Record massPoint: Type := cons { number: R; point: Point}.
Variable add_MP: massPoint -> massPoint -> massPoint.
Variable sub_MP: massPoint -> massPoint -> massPoint.
Definition isVector (v : massPoint) :=
exists A B : Point, v = add_MP (cons (-1) A) (cons 1 B).
Record Vector : Type := vecCons { mpOf : massPoint; proof : isVector mpOf }.
Definition point_sub (p1 p2: massPoint) : Vector.
Proof.
refine (vecCons (sub_MP p1 p2) _).
repeat eexists.
answered Nov 25 '18 at 3:59
ejgallegoejgallego
5,3641925
It looks like Coq cannot find the supporting mass point A and B. So I think it should beDefinition point_sub (p1 p2: massPoint) : Vector := vecCons (sub_MP p1 p2) add_MP (cons (-1) (point p1))(cons 1 (point p2)).But coq kernel is still complainingwhile it is expected to have type "isVector (sub_MP p1 p2)".I feel like I don't have enough commands in my proof repertoire to tackle it. Or I didn't understand your hint well enough. If possible, could you please elaborate a bit? Much appreciate your way of giving hints.
– isPrime
Nov 25 '18 at 4:46
You need to find ?A ?B such that ` sub_MP p1 p2 = add_MP {| number := -1; point := ?A |} {| number := 1; point := ?B |}` The way you write the above term doesn't make sense to the Coq typer, you are expected to write a term with the above type.
– ejgallego
Nov 25 '18 at 5:20
Honestly, the syntax is exactly the help I need. I can’t figure out how to write it in a way that Coq understands. I still lack the knowledge of it. If you decide to write it out, would you please also explain why the syntax is written that way? I want to understand the connections.
– isPrime
Nov 25 '18 at 15:31
You need to proveLemma my_proof : exists A B, sub_MP p1 p2 = add_MP {| number := -1; point := A |} {| number := 1; point := B |}, then you can usemy_proofin the construction of your record. But I'd say you need to take a course in Coq first, so you learn the basic syntax and typing rules first.
– ejgallego
Nov 25 '18 at 16:31
1
Thanks for the further hint. I'm able to construct that new record using the following syntaxDefinition mp_sub (p1 p2: massPoint) : Vector:= vecCons (sub_MP p1 p2) (mp_proof p1 p2).
– isPrime
Nov 25 '18 at 17:48
add a comment |
2
You are having basic instantiation problems with regards on what a proof is. See for example this code and try to understand what you are missing:
Require Import Coq.Reals.Reals.
Open Scope R_scope.
Definition Point := Type.
Record massPoint: Type := cons { number: R; point: Point}.
Variable add_MP: massPoint -> massPoint -> massPoint.
Variable sub_MP: massPoint -> massPoint -> massPoint.
Definition isVector (v : massPoint) :=
exists A B : Point, v = add_MP (cons (-1) A) (cons 1 B).
Record Vector : Type := vecCons { mpOf : massPoint; proof : isVector mpOf }.
Definition point_sub (p1 p2: massPoint) : Vector.
Proof.
refine (vecCons (sub_MP p1 p2) _).
repeat eexists.
answered Nov 25 '18 at 3:59
ejgallegoejgallego
5,3641925
It looks like Coq cannot find the supporting mass point A and B. So I think it should beDefinition point_sub (p1 p2: massPoint) : Vector := vecCons (sub_MP p1 p2) add_MP (cons (-1) (point p1))(cons 1 (point p2)).But coq kernel is still complainingwhile it is expected to have type "isVector (sub_MP p1 p2)".I feel like I don't have enough commands in my proof repertoire to tackle it. Or I didn't understand your hint well enough. If possible, could you please elaborate a bit? Much appreciate your way of giving hints.
– isPrime
Nov 25 '18 at 4:46
You need to find ?A ?B such that ` sub_MP p1 p2 = add_MP {| number := -1; point := ?A |} {| number := 1; point := ?B |}` The way you write the above term doesn't make sense to the Coq typer, you are expected to write a term with the above type.
– ejgallego
Nov 25 '18 at 5:20
Honestly, the syntax is exactly the help I need. I can’t figure out how to write it in a way that Coq understands. I still lack the knowledge of it. If you decide to write it out, would you please also explain why the syntax is written that way? I want to understand the connections.
– isPrime
Nov 25 '18 at 15:31
You need to proveLemma my_proof : exists A B, sub_MP p1 p2 = add_MP {| number := -1; point := A |} {| number := 1; point := B |}, then you can usemy_proofin the construction of your record. But I'd say you need to take a course in Coq first, so you learn the basic syntax and typing rules first.
– ejgallego
Nov 25 '18 at 16:31
1
Thanks for the further hint. I'm able to construct that new record using the following syntaxDefinition mp_sub (p1 p2: massPoint) : Vector:= vecCons (sub_MP p1 p2) (mp_proof p1 p2).
– isPrime
Nov 25 '18 at 17:48
add a comment |
2
2
2
You are having basic instantiation problems with regards on what a proof is. See for example this code and try to understand what you are missing:
Require Import Coq.Reals.Reals.
Open Scope R_scope.
Definition Point := Type.
Record massPoint: Type := cons { number: R; point: Point}.
Variable add_MP: massPoint -> massPoint -> massPoint.
Variable sub_MP: massPoint -> massPoint -> massPoint.
Definition isVector (v : massPoint) :=
exists A B : Point, v = add_MP (cons (-1) A) (cons 1 B).
Record Vector : Type := vecCons { mpOf : massPoint; proof : isVector mpOf }.
Definition point_sub (p1 p2: massPoint) : Vector.
Proof.
refine (vecCons (sub_MP p1 p2) _).
repeat eexists.
answered Nov 25 '18 at 3:59
ejgallegoejgallego
5,3641925
You are having basic instantiation problems with regards on what a proof is. See for example this code and try to understand what you are missing:
Require Import Coq.Reals.Reals.
Open Scope R_scope.
Definition Point := Type.
Record massPoint: Type := cons { number: R; point: Point}.
Variable add_MP: massPoint -> massPoint -> massPoint.
Variable sub_MP: massPoint -> massPoint -> massPoint.
Definition isVector (v : massPoint) :=
exists A B : Point, v = add_MP (cons (-1) A) (cons 1 B).
Record Vector : Type := vecCons { mpOf : massPoint; proof : isVector mpOf }.
Definition point_sub (p1 p2: massPoint) : Vector.
Proof.
refine (vecCons (sub_MP p1 p2) _).
repeat eexists.
answered Nov 25 '18 at 3:59
ejgallegoejgallego
5,3641925
answered Nov 25 '18 at 3:59
ejgallegoejgallego
5,3641925
answered Nov 25 '18 at 3:59
ejgallegoejgallego
5,3641925
answered Nov 25 '18 at 3:59
ejgallegoejgallego
5,3641925
5,3641925
It looks like Coq cannot find the supporting mass point A and B. So I think it should beDefinition point_sub (p1 p2: massPoint) : Vector := vecCons (sub_MP p1 p2) add_MP (cons (-1) (point p1))(cons 1 (point p2)).But coq kernel is still complainingwhile it is expected to have type "isVector (sub_MP p1 p2)".I feel like I don't have enough commands in my proof repertoire to tackle it. Or I didn't understand your hint well enough. If possible, could you please elaborate a bit? Much appreciate your way of giving hints.
– isPrime
Nov 25 '18 at 4:46
You need to find ?A ?B such that ` sub_MP p1 p2 = add_MP {| number := -1; point := ?A |} {| number := 1; point := ?B |}` The way you write the above term doesn't make sense to the Coq typer, you are expected to write a term with the above type.
– ejgallego
Nov 25 '18 at 5:20
Honestly, the syntax is exactly the help I need. I can’t figure out how to write it in a way that Coq understands. I still lack the knowledge of it. If you decide to write it out, would you please also explain why the syntax is written that way? I want to understand the connections.
– isPrime
Nov 25 '18 at 15:31
You need to proveLemma my_proof : exists A B, sub_MP p1 p2 = add_MP {| number := -1; point := A |} {| number := 1; point := B |}, then you can usemy_proofin the construction of your record. But I'd say you need to take a course in Coq first, so you learn the basic syntax and typing rules first.
– ejgallego
Nov 25 '18 at 16:31
1
Thanks for the further hint. I'm able to construct that new record using the following syntaxDefinition mp_sub (p1 p2: massPoint) : Vector:= vecCons (sub_MP p1 p2) (mp_proof p1 p2).
– isPrime
Nov 25 '18 at 17:48
add a comment |
It looks like Coq cannot find the supporting mass point A and B. So I think it should beDefinition point_sub (p1 p2: massPoint) : Vector := vecCons (sub_MP p1 p2) add_MP (cons (-1) (point p1))(cons 1 (point p2)).But coq kernel is still complainingwhile it is expected to have type "isVector (sub_MP p1 p2)".I feel like I don't have enough commands in my proof repertoire to tackle it. Or I didn't understand your hint well enough. If possible, could you please elaborate a bit? Much appreciate your way of giving hints.
– isPrime
Nov 25 '18 at 4:46
You need to find ?A ?B such that ` sub_MP p1 p2 = add_MP {| number := -1; point := ?A |} {| number := 1; point := ?B |}` The way you write the above term doesn't make sense to the Coq typer, you are expected to write a term with the above type.
– ejgallego
Nov 25 '18 at 5:20
Honestly, the syntax is exactly the help I need. I can’t figure out how to write it in a way that Coq understands. I still lack the knowledge of it. If you decide to write it out, would you please also explain why the syntax is written that way? I want to understand the connections.
– isPrime
Nov 25 '18 at 15:31
You need to proveLemma my_proof : exists A B, sub_MP p1 p2 = add_MP {| number := -1; point := A |} {| number := 1; point := B |}, then you can usemy_proofin the construction of your record. But I'd say you need to take a course in Coq first, so you learn the basic syntax and typing rules first.
– ejgallego
Nov 25 '18 at 16:31
1
Thanks for the further hint. I'm able to construct that new record using the following syntaxDefinition mp_sub (p1 p2: massPoint) : Vector:= vecCons (sub_MP p1 p2) (mp_proof p1 p2).
– isPrime
Nov 25 '18 at 17:48
It looks like Coq cannot find the supporting mass point A and B. So I think it should be
Definition point_sub (p1 p2: massPoint) : Vector := vecCons (sub_MP p1 p2) add_MP (cons (-1) (point p1))(cons 1 (point p2)). But coq kernel is still complaining while it is expected to have type "isVector (sub_MP p1 p2)". I feel like I don't have enough commands in my proof repertoire to tackle it. Or I didn't understand your hint well enough. If possible, could you please elaborate a bit? Much appreciate your way of giving hints.– isPrime
Nov 25 '18 at 4:46
It looks like Coq cannot find the supporting mass point A and B. So I think it should be
Definition point_sub (p1 p2: massPoint) : Vector := vecCons (sub_MP p1 p2) add_MP (cons (-1) (point p1))(cons 1 (point p2)). But coq kernel is still complaining while it is expected to have type "isVector (sub_MP p1 p2)". I feel like I don't have enough commands in my proof repertoire to tackle it. Or I didn't understand your hint well enough. If possible, could you please elaborate a bit? Much appreciate your way of giving hints.– isPrime
Nov 25 '18 at 4:46
You need to find ?A ?B such that ` sub_MP p1 p2 = add_MP {| number := -1; point := ?A |} {| number := 1; point := ?B |}` The way you write the above term doesn't make sense to the Coq typer, you are expected to write a term with the above type.
– ejgallego
Nov 25 '18 at 5:20
You need to find ?A ?B such that ` sub_MP p1 p2 = add_MP {| number := -1; point := ?A |} {| number := 1; point := ?B |}` The way you write the above term doesn't make sense to the Coq typer, you are expected to write a term with the above type.
– ejgallego
Nov 25 '18 at 5:20
Honestly, the syntax is exactly the help I need. I can’t figure out how to write it in a way that Coq understands. I still lack the knowledge of it. If you decide to write it out, would you please also explain why the syntax is written that way? I want to understand the connections.
– isPrime
Nov 25 '18 at 15:31
Honestly, the syntax is exactly the help I need. I can’t figure out how to write it in a way that Coq understands. I still lack the knowledge of it. If you decide to write it out, would you please also explain why the syntax is written that way? I want to understand the connections.
– isPrime
Nov 25 '18 at 15:31
You need to prove
Lemma my_proof : exists A B, sub_MP p1 p2 = add_MP {| number := -1; point := A |} {| number := 1; point := B |}, then you can use my_proof in the construction of your record. But I'd say you need to take a course in Coq first, so you learn the basic syntax and typing rules first.– ejgallego
Nov 25 '18 at 16:31
You need to prove
Lemma my_proof : exists A B, sub_MP p1 p2 = add_MP {| number := -1; point := A |} {| number := 1; point := B |}, then you can use my_proof in the construction of your record. But I'd say you need to take a course in Coq first, so you learn the basic syntax and typing rules first.– ejgallego
Nov 25 '18 at 16:31
1
1
Thanks for the further hint. I'm able to construct that new record using the following syntax
Definition mp_sub (p1 p2: massPoint) : Vector:= vecCons (sub_MP p1 p2) (mp_proof p1 p2).– isPrime
Nov 25 '18 at 17:48
Thanks for the further hint. I'm able to construct that new record using the following syntax
Definition mp_sub (p1 p2: massPoint) : Vector:= vecCons (sub_MP p1 p2) (mp_proof p1 p2).– isPrime
Nov 25 '18 at 17:48
add a comment |
draft saved
draft discarded
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
draft saved
draft discarded
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53464448%2fconstruct-a-new-record-instances-when-the-record-type-has-dependent-binders-in-c%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
